Z/Eves and the Mondex Electronic Purse
Z/Eves and the Mondex Electronic Purse
复制标题
Z/Eves 和 Mondex 电子钱包
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
Leo Freitas
中科院分区：
文献类型：
--
作者：
J. Woodcock;Leo Freitas
我们描述了我们使用 Z/Eves 定理证明器对 Mondex 电子钱包进行规范、细化和证明的机械化经验。我们采取了保守的方法，机械化了原始的${sc L^{A}T_{E}X}$来源，除了纠正错误之外，没有改变其技术内容：我们发现了原始文本中的问题，并在改进中缺少了不变量。基于这些经验，我们针对如何成功推动 Z/Eves 提供了新颖且详细的指导。这项工作有助于实现为验证软件大挑战构建存储库的研究目标。
We describe our experiences in mechanising the specification, refinement, and proof of the Mondex Electronic Purse using the Z/Eves theorem prover. We took a conservative approach and mechanised the original ${sc L^{A}T_{E}X}$ sources, without changing their technical content, except to correct errors: we found problems in the original texts and missing invariants in the refinements. Based on these experiences, we present novel and detailed guidance on how to drive Z/Eves successfully. The work contributes to the research objectives of building the Repository for the Verified Software Grand Challenge.