TLA+
Sign in to saveAlso known as TLA⁺
TLA+ is a formal specification language developed by Leslie Lamport. It is used for designing, modelling, documentation, and verification of programs, especially concurrent systems and distributed systems. TLA+ is considered to be exhaustively-testable pseudocode,
Wikidata facts
- Official website
- lamport.azurewebsites.net/tla/tla.html
Show 1 more fact
- inception
- 1999-04-23
Sources (1)
via Wikidata · CC0
~22 min read
Article
16 sectionsContents
- History
- Language
- Safety
- Liveness
- Operators
- Data structures
- Standard modules
- Tools
- IDE
- Model checker
- Proof system
- Industry use
- Examples
- =
- See also
- References
TLA+ is a formal specification language developed by Leslie Lamport. It is used for designing, modelling, documentation, and verification of programs, especially concurrent systems and distributed systems. TLA+ is considered to be exhaustively-testable pseudocode, and its use likened to drawing blueprints for software systems; TLA is an acronym for Temporal Logic of Actions.
For design and documentation, TLA+ fulfills the same purpose as informal technical specifications. However, TLA+ specifications are written in a formal language of logic and mathematics, and the precision of specifications written in this language is intended to uncover design flaws before system implementation is underway.