プラスカル

PlusCal（旧称+CAL ）は、 Leslie Lamportによって作成された形式仕様言語で、TLA ⁺にトランスパイルされます。TLA ⁺が分散システムへのアクション指向に重点を置いているのに対し、PlusCal は命令型プログラミング言語に最も似ており、逐次アルゴリズムの仕様を記述するのに適しています。^{[ 1 ]} PlusCal は擬似コードを置き換えるために設計されており、そのシンプルさを維持しながら、形式的に定義され検証可能な言語を提供しています。^{[ 2 ]} 1ビットクロックは、PlusCal で次のように記述されます。

-- 公平なアルゴリズム OneBitClock { 変数クロック \in {0, 1}; { (TRUE) { (クロック = 0)の場合 クロック:= 1 それ以外 クロック:= 0 } } } 

参照

• フィズビー
• TLA ⁺
• 擬似コード

参考文献

1. Lamport, Leslie (2015年2月28日). Principles and Specifications of Concurrent Systems . p. 7 . 2015年5月10日閲覧。PlusCalは、アルゴリズムの制御フローを記述するのにTLA ⁺よりも便利です。そのため、一般的に、逐次アルゴリズムや共有メモリ型マルチプロセスアルゴリズムの仕様記述に適しています。
2. ランポート、レスリー(2009年1月2日). 「PlusCalアルゴリズム言語」(PDF) .コンピューティングの理論的側面 - ICTAC 2009.コンピュータサイエンス講義ノート. 第5684巻. シュプリンガー・ベルリン・ハイデルベルク. pp.  36– 60. doi : 10.1007/978-3-642-03466-4_2 . ISBN 978-3-642-03465-7. 2015年5月10日閲覧。

外部リンク

• PlusCal ツールとドキュメントは、 PlusCal アルゴリズム言語ページにあります。