文章基本信息

标题：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の相互排除性の検証を例として，証明譜を用いた検証法の原理や仕組みを説明するとともに，証明譜の記述の技法も解説する．