노트
Learn TLA+에 온 것을 환영한다! 아직 작업 중이니 업데이트 소식은 새 소식을 참고하고, 질문이나 걱정되는 점이 있으면 GitHub 저장소에 올려 주기 바란다. 여러분의 피드백을 꼭 듣고 싶다!
(그동안 옛 버전은 old.learntla.com에서 볼 수 있다.)
Learn TLA+
한국어판 안내
이 사이트는 Hillel Wayne의 『Learn TLA+』(learntla.com) 전체 35페이지를 원저작물의 CC BY 4.0 라이선스에 따라 한국어로 옮긴 것이다. TLA+·PlusCal 코드, 내려받는 스펙 파일, 툴박스 스크린샷은 원문 그대로 두었고, 용어는 페이지마다 처음 나올 때 한국어(English)로 병기했다.
책 전체를 한 페이지로 훑고 싶다면 원페이지 요약부터 읽어도 된다.
소프트웨어 결함은 대부분 두 곳 중 하나에서 나온다. 코드 버그는 코드가 설계와 어긋나는 경우다 — 예를 들면 off-by-one 오류나 널 역참조가 그렇다. 코드 버그를 찾는 기법은 많다. 그렇다면 설계 결함은 어떨까? 설계상의 버그에 관해서라면, 우리가 배우는 것은 “정말 열심히 생각해 보라”는 말뿐이다.
TLA+는 “정형 명세 언어(formal specification language)”, 즉 설계를 직접 테스트해 볼 수 있게 해 주는 시스템 설계 수단이다. 튜링상 수상자 레슬리 램포트(Leslie Lamport)가 개발한 TLA+는 AWS, Microsoft, CrowdStrike 같은 기업들의 지지를 받아 왔다. TLA+는 엔지니어링 역량을 대체하는 게 아니라 보강한다. TLA+를 쓰면 시스템을 더 빠르고 더 자신 있게 설계할 수 있다. 실제로 적용된 예를 보고 싶다면 개념 개요를 살펴보자.
이 가이드에 대하여
이곳은 TLA+를 배우기 위한 무료 온라인 자료다. 초보자와 숙련된 사용자를 모두 돕기 위해 가이드를 세 부분으로 나누었다:
핵심 과정: TLA+ 언어 전체를 순서대로 소개하는 입문이다. 기본 연산자(operator)에서 출발해 점차 고급 주제까지 나아간다. 핵심 과정은 순서대로 읽도록 만들었다: TLA+가 처음인 사람은 개념 개요에서 시작해 거기서부터 차례로 읽어 나가면 된다. TLA+에 익숙한 사람은 새로운 내용이 나올 때까지 훑어보면 된다.
주제별 심화: “선택 사항”인 고급 자료다. 각 레슨은 TLA+ 사용자 다수에게는 쓸모가 있겠지만 전부에게 그렇지는 않을 것이다. 핵심 과정과 달리 이 레슨들은 대체로 서로 독립적이도록 설계했다. 어떤 주제가 다른 주제에 의존한다면 그 점을 따로 밝혀 두겠다.
예제: TLA+를 스펙(spec)에 적용한 사례들로, 스펙을 작성하는 법과 이해하는 법을 모두 보여 준다.
이 가이드는 아직 개발 중이니, 최신 업데이트는 새 소식에서, 내가 지금 작업하고 있는 내용은 로드맵에서 확인하자.
나에 대하여
나는 힐렐(Hillel)이다. TLA+ 재단의 일원이자 Practical TLA+라는 책의 저자다. TLA+를 누구나 최대한 쉽게 접할 수 있기를 바라는데, 내 책은 돈을 내야 볼 수 있다는 점이 마음에 들지 않아서 이 가이드를 썼다. 블로그와 주간 뉴스레터도 운영하고 있다.
(솔직히 밝혀 두자면, 나는 전문 TLA+ 컨설턴트이기도 하고 <광고>워크숍도 진행한다</광고>.)
이 책의 차례
핵심 과정
- 핵심 과정 Core
- 환경 설정 Setup
- 연산자와 값 Operators and Values
- 스펙 작성하기 Writing Specifications
- 불변식 작성하기 Writing an Invariant
- 스펙 매개변수화 Parameterizing Specs
- 구조화된 데이터 Structured Data
- 비결정성 Nondeterminism
- 동시성 Concurrency
- 시간 속성 Temporal Properties
- 연산자 더 알아보기 More Operators
- 액션 속성 Action Properties
- TLA+ TLA+
- 모듈 Modules
- 다음 단계 Next Steps
주제별 심화