「PlusCal」の版間の差分
削除された内容 追加された内容
Darklanlan (会話 | 投稿記録) m +stub |
Darklanlan (会話 | 投稿記録) 翻訳元より出典を追加（履歴継承不要） +孤立 |
||
| 1行目: | 1行目: | ||
{{孤立|date=2016年12月}} |
|||
'''PlusCal ('''旧称 '''+CAL''') は、 [[レスリー・ランポート|Leslie Lamppost]] により考案された形式仕様言語で |
'''PlusCal ('''旧称 '''+CAL''') は、 [[レスリー・ランポート|Leslie Lamppost]] により考案された形式仕様言語で、 TLA<sup>+</sup> に変換される。TLA<sup>+ </sup>のアクション志向が分散システムに重点を置いているのとは異なり、 PlusCalは逐次命令形のプログラミング言語と似ており、シーケンシャルアルゴリズムの記述により適している<ref name="hyperbook-pluscal"> |
||
| ⚫ | |||
{{cite book |
|||
| last = Lamport |
|||
| first = Leslie |
|||
| authorlink = Leslie Lamport |
|||
| date = 28 February 2015 |
|||
| title = Principles and Specifications of Concurrent Systems |
|||
| url= http://research.microsoft.com/en-us/um/people/lamport/tla/hyperbook.html |
|||
| page= 7 |
|||
| quote = "PlusCal is more convenient than TLA<sup>+</sup> for describing the flow of control in an algorithm. This generally makes it better for specifying sequential algorithms and shared-memory multiprocess algorithms." |
|||
| accessdate = 10 May 2015}} |
|||
</ref>。PlusCalは [[擬似コード]] を置き換えることを目的に設計されており、その簡潔性を維持する一方で形式的に定義され検証可能な言語を提供している<ref name="pluscal-original"> |
|||
{{cite journal |
|||
| last = Lamport |
|||
| first = Leslie |
|||
| authorlink = Leslie Lamport |
|||
| title = The PlusCal Algorithm Language |
|||
| journal = Lecture Notes in Computer Science |
|||
| volume = 5684 |
|||
| issue = Theoretical Aspects of Computing - ICTAC 2009 |
|||
| pages = 36–60 |
|||
| publisher = Springer Berlin Heidelberg |
|||
| date = 2 January 2009 |
|||
| url = http://research.microsoft.com/en-us/um/people/lamport/pubs/pluscal.pdf |
|||
| doi = 10.1007/978-3-642-03466-4_2 |
|||
| accessdate = 10 May 2015 }} |
|||
</ref>。 |
|||
| ⚫ | |||
-- fair algorithm OneBitClock { |
-- fair algorithm OneBitClock { |
||
variable clock \in {0, 1}; |
variable clock \in {0, 1}; |
||
| 14行目: | 42行目: | ||
</syntaxhighlight>PlusCalのツールとドキュメントは [http://research.microsoft.com/en-us/um/people/lamport/tla/pluscal.html PlusCalアルゴリズム言語のページ] から参照することができる． |
</syntaxhighlight>PlusCalのツールとドキュメントは [http://research.microsoft.com/en-us/um/people/lamport/tla/pluscal.html PlusCalアルゴリズム言語のページ] から参照することができる． |
||
== |
== 関連項目 == |
||
* TLA<sup>+</sup> |
* TLA<sup>+</sup> |
||
* [[擬似コード|Pseudocode]] |
* [[擬似コード|Pseudocode]] |
||
== |
== 脚注 == |
||
{{reflist}} |
|||
[[Category:形式手法]] |
[[Category:形式手法]] |
||
2016年12月3日 (土) 11:55時点における版
 |
PlusCal (旧称 +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 (2 January 2009). “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日閲覧。.
 | この項目は、コンピュータに関連した書きかけの項目です。この項目を加筆・訂正などしてくださる協力者を求めています（PJ:コンピュータ/P:コンピュータ）。 |