• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>International Conference on Rigorous State-Based Methods >Existence Proof Obligations for Constraints, Properties and Invariants in Atelier B
【24h】

Existence Proof Obligations for Constraints, Properties and Invariants in Atelier B

机译：工作室B中约束，属性和不变量的存在证明义务

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Proof obligations of the B method and of Event B use predicates in the Constraints, Sets, Properties and Invariant clauses as hypotheses in proof obligations. A contradiction in these predicates results in trivially valid proof obligations and essentially voids the development. A textbook on the B method [3] presents three "existence proof obligations" to show the satisfiability of the Constraints, Properties and Invariant clauses as soon as they are stated in a component. Together with new existence proof obligations for refinement, this prevents the introduction of such contradictions in the refinement chain. This paper presents a detailed formalization of these existence proof obligations, specifying their implementation in Atelier B.
机译：B方法和事件B的证明义务使用“约束”，“集合”，“属性”和“不变”子句中的谓词作为证明义务的假设。这些谓词中的矛盾导致琐碎有效的证明义务，并实质上使开发无效。关于B方法的教科书[3]提出了三种“存在证明义务”，以表明约束，属性和不变子句在组件中一经陈述就可满足。再加上对提炼的新的存在证明义务，这可以防止在精炼链中引入此类矛盾。本文详细介绍了这些存在证明义务，并详细说明了在Atelier B中的执行情况。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号