|Designed by||Leslie Lamport|
|First appeared||April 30, 1994|
|TLA+2 / January 15, 2014|
TLA+ (styled as TLA+) is a formal specification language originally developed by Leslie Lamport for specifying concurrent and distributed systems and algorithms. It is based on the temporal logic TLA (also introduced by Lamport) for the description of the system's behavior and on standard set theory for representing data structures.
TLA+ specifications and their properties are both written as formulas in the same logical language. Specifications are organized in modules that contain declarations of variables and constants, definitions of operators, and assertions of assumptions and theorems.
In addition, TLA+ is extended with a notation for writing hierarchical proofs, which can be interpreted by TLAPS.
- Official TLA homepage
- TLC model-checker
- TLA+ Proof System
- TLA+ Toolbox
- Leslie Lamport, Thinking for Programmers, a gentle intro to TLA+ at Build 2014.
|This formal methods-related article is a stub. You can help Wikipedia by expanding it.|