TLA+
TLAは、アルゴリズムと数学的定理の両方について、マシンでチェックされた正確性の証明を作成するためにも使用される。証明は、単一の定理証明者バックエンドに依存しない宣言型の階層スタイルで記述される。公式および非公式の構造化された数学的証明は、TLAで記述できる。言語はLaTeXに似ており、TLAのコードをLaTeXドキュメントに翻訳するためのツールが存在する。
TLAは、並行システムの検証方法に関する数十年の研究の後、1999年に公開された。その後、IDEや分散モデルチェッカーなどのツールチェーンが開発された。擬似コードのような言語PlusCalは2009年に作成され、TLAにトランスパイルされ、シーケンシャルアルゴリズムを記述する際に有用とされる。 TLAは2014年に発表され、プルーフコンストラクトの言語サポートを拡張した。現在のTLAリファレンスは、LeslieLamportによるTLAHyperbookである。
TLAの基本的なデータ構造とは集合である。集合は、明示的に列挙されるか、演算子を使用するか、 {x \in S : p} (pはxの条件)または{e : x \in S} (eはxの関数)を使用して他の集合から構築される。一意の空集合は{}として表される。
TLAの関数は、ドメイン内の各要素集合に値を割り当てる。 [S -> T]は、定義域集合Sの各xについて、Tにf [x]を持つすべての関数の集合である。例えばTLA関数Double[x \in Nat] == x*2 とは集合 [Nat -> Nat]の一要素であるため、 Double \in [Nat -> Nat]はTLAの真のステートメントである。関数は、一部の式e [x \in S |-> e]を使用するか、既存の関数を変更することによっても定義される[f EXCEPT ![v 1 ] = v 2 ] 。
レコードはTLAの関数の一種である。レコード[name |-> "John", age |-> 35]は、フィールドnameとageを持つレコードであり、 r.nameやr.ageでアクセスされ、レコードの集合[name : String, age : Nat]に所属する。
タプルはTLAに含まれている。 <<e 1 ,e 2 ,e 3 >>は明示的に定義されるか、標準のシーケンスモジュールの演算子で構成される。タプルの集合は、デカルト積によって定義される。たとえば、自然数のすべてのペアの集合は、 Nat \X Natとして定義される。