TLA+
TLAコードは複数のモジュールからなる。モジュールは、他のモジュールを拡張(インポート)して、その機能を使用できる。 TLA標準はタイプセット数学記号で指定されているが、既存のTLAツールは、ASCIIでLaTeXのような記号定義を使用する。 TLAでは、定義が必要ないくつかの用語を使用する。
State – 変数への値の代入
Behaviour – 連続したState
Step – Behaviourでの連続したStateのペア
Shuttering step – 変数が変更されないStep
Next-state relation – 変数が任意のStepでどのように変化するかを説明する関係
State function – Next-state relationではない変数と定数を含む式
State predicate – ブール値の状態関数
Invariant – 到達可能なすべてのStateで真とする状態述語
Temporal formula – 時相論理のステートメントを含む式
TLAは、すべての正しいシステム動作のBehaviorを定義することを目的としている。例えば、0と1の間で際限なく刻々と変化する1ビットクロックは、次のように記述できる。
Relation Tickはクロックが1であればclock'(次のStateにおけるclockの値)は0、0であれば1を設定する。clockの値が0または1の場合、State PredicateであるInitはtrueである。 Specは、1ビットクロックのすべてのBehaviorが最初にInitを満たし、すべてのStepがTickに一致するか、Shuttering stepである必要があることをアサートするTemporal formulaである。そのような2つの動作は次の通りである。
1ビットクロックの安全性は –到達可能なシステム状態の集合 –という仕様によって適切に説明される。