官方网站:The TLA+ Home Page by Leslie Lamport
Terminology
TLA:时序逻辑行为(Temporal Logic of Actions)
TLC:遍历 TLA+ 抽象出来的系统的每一个可能路径,并在每条可能的路径上对一些条件(称为“不变式”)进行检验。
Demos
SimpleProgram
对以下 C 语言代码进行验证:
1 |
|

DieHard

TCommit
两阶段提交

TwoPhase
Arrays in TLA+
Syntax
The TLA+ syntax for an array expression:
For example:
Defines
Terminology
Programming | Math | TLA+ |
---|---|---|
array | function | function |
index set | domain | domain |
Math and TLA+ allows a function to have any set as its domain — for exxample, the set of all integers.
Abbreviation
Signal

Math | Code |
---|---|
/\ , \land |
|
\/ , \lor |
|
\E |
|
\A |
|
\in |
|
` | |
-> |
|
>= |
|
=< |
|
== |
|
/= , # |
|
~ |
|
\cap , \union |
|
<< |