PlusCal
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2018/10/03 09:05 UTC 版)
Jump to navigation Jump to searchPlusCal (旧称 +CAL) は、 Leslie Lamppost により考案された形式仕様言語で、 TLA+ に変換される。TLA+ のアクション志向が分散システムに重点を置いているのとは異なり、 PlusCalは逐次命令形のプログラミング言語と似ており、シーケンシャルアルゴリズムの記述により適している[1]。PlusCalは 擬似コード を置き換えることを目的に設計されており、その簡潔性を維持する一方で形式的に定義され検証可能な言語を提供している[2]。
例として、1ビットクロックはPlusCalでは次のようにかける。
-- fair algorithm OneBitClock {
variable clock \in {0, 1};
{
while (TRUE) {
if (b = 0)
b := 1
else
b := 0
}
}
}
PlusCalのツールとドキュメントは PlusCalアルゴリズム言語のページ から参照することができる.
関連項目
- TLA+
- Pseudocode
脚注
- ^ Lamport, Leslie (28 February 2015). Principles and Specifications of Concurrent Systems. p. 7 2015年5月10日閲覧. ""PlusCal is more convenient than TLA+ for describing the flow of control in an algorithm. This generally makes it better for specifying sequential algorithms and shared-memory multiprocess algorithms.""
- ^ Lamport, Leslie (2009年1月2日). “The PlusCal Algorithm Language”. Lecture Notes in Computer Science (Springer Berlin Heidelberg) 5684 (Theoretical Aspects of Computing - ICTAC 2009): 36–60. doi:10.1007/978-3-642-03466-4_2 2015年5月10日閲覧。.
- PlusCalのページへのリンク