文章基本信息
- 标题：CafeOBJ入門(4) 証明譜による検証法
- 本地全文：下载
- 作者：二木 厚吉 ; 緒方 和博 ; 中村 正樹 等
- 期刊名称：コンピュータ ソフトウェア
- 印刷版ISSN：0289-6540
- 出版年度：2008
- 卷号：25
- 期号：4
- 页码：4_68-4_84
- DOI：10.11309/jssst.25.4_68
- 出版社：Japan Society for Software Science and Technology
- 摘要：
証明譜を用いた簡約のみに基づくCafeOBJの検証法を解説する．待ち行列を用いる相互排除プロトコルQlockの相互排除性の検証を例として，証明譜を用いた検証法の原理や仕組みを説明するとともに，証明譜の記述の技法も解説する．
