TLA+
ウィキペディア フリーな encyclopedia
TLA+は、Leslie Lamportによって開発された形式仕様言語。並行システムと分散システムの設計、モデル化、文書化、および検証に使用される。 TLA+は、網羅的にテスト可能な擬似コード[4]として説明されており、その使用はソフトウェアシステムの設計図を描くことに喩えられる。 [5] TLAはTemporal Logic of Actionsの頭字語である。
パラダイム | Action |
---|---|
登場時期 |
1999年4月23日 (25年前) (1999-04-23) [1] |
設計者 | Leslie Lamport |
最新リリース | TLA+2/ 2014年1月15日 (10年前) (2014-01-15)[2] |
プラットフォーム | Cross-platform (multi-platform) |
ライセンス | MIT License[3] |
ウェブサイト |
research |
拡張子 | .tla |
テンプレートを表示 |
設計と文書化に関して、TLA+ は非公式の技術仕様と同じ目的を果たす。ただし、TLA+の仕様は論理学と数学の形式言語で記述されており、この言語で記述された仕様の精度は、システムの実装が始まる前に設計上の欠陥を明らかにすることを目的としている。 [6]
TLA+のコードは形式言語で記述するため、有限モデル検査に適する。モデルチェッカーは、いくつかの実行ステップまでのすべての可能なシステム動作を見つけ、安全性や活性などの望ましい不変性プロパティの違反を調べる。 TLA+のコードでは、基本的な集合論を使用して安全性(悪いことが起こらない事)を定義し、時相論理を使用して活性(良いことがいずれ起こる事)を定義する。
TLA+は、アルゴリズムと数学的定理の両方について、マシンでチェックされた正確性の証明を作成するためにも使用される。証明は、単一の定理証明者バックエンドに依存しない宣言型の階層スタイルで記述される。公式および非公式の構造化された数学的証明は、TLA+で記述できる。言語はLaTeXに似ており、TLA+のコードをLaTeXドキュメントに翻訳するためのツールが存在する。 [7]
TLA+は、並行システムの検証方法に関する数十年の研究の後、1999年に公開された。その後、IDEや分散モデルチェッカーなどのツールチェーンが開発された。擬似コードのような言語PlusCalは2009年に作成され、TLA+にトランスパイルされ、シーケンシャルアルゴリズムを記述する際に有用とされる。 TLA+2は2014年に発表され、プルーフコンストラクトの言語サポートを拡張した。現在のTLA+リファレンスは、LeslieLamportによるTLA+Hyperbookである。