VDM操作证明义务生成的进一步进展
Further Progress Towards Operation Proof Obligation Generation for VDM
浏览论文内容
中文总结 AI 辅助
本文更新VDM操作证明义务生成的相关工作，改进循环不变式等处理方法并新增多项功能，通过示例说明新特性，推进VDM形式化方法的证明义务生成研究。
中文摘要 AI 辅助
VDM形式化方法可确保模型内部一致性，称为证明义务的断言会突出潜在不一致性。本文是对文献[1]中关于VDM操作的证明义务生成工作的更新，呈现了最新研究：改进了循环不变式处理方法，新增循环变体，完善了操作调用（包括隐式声明操作和规约语句）的证明义务，新增操作的递归度量，并通过示例说明这些新特性。
英文摘要
The VDM formalism can ensure that models are internally consistent. Potential inconsistencies are highlighted by assertions called proof obligations. This paper is an update to the work described in [1], regarding proof obligation generation for VDM operations. We present the latest work which improves the approach to loop invariants, adds loop variants, improves proof obligations for operation calls, including implicitly declared operations and specification statements, and adds recursive measures for operations. The new features are illustrated with examples.
