计算机应用 ›› 2011, Vol. 31 ›› Issue (05): 1425-1427.DOI: 10.3724/SP.J.1087.2011.01425

• 典型应用 • 上一篇    下一篇

基于Kripke结构的程序正确性证明

林杰,余建坤   

  1. 云南财经大学 信息学院,昆明 650221
  • 收稿日期:2010-10-20 修回日期:2010-12-09 发布日期:2011-05-01 出版日期:2011-05-01
  • 通讯作者: 余建坤
  • 作者简介:林杰(1987-),男,福建龙岩人,硕士研究生,主要研究方向:商务智能、数据挖掘;余建坤(1962-),男,云南开远人,教授,硕士,主要研究方向:商务智能、数据挖掘。

Proof of program correctness based on Kripke structure

LIN Jie, YU Jian-kun   

  1. Information School, Yunnan University of Finance and Economics, Kunming Yunnan 650221, China
  • Received:2010-10-20 Revised:2010-12-09 Online:2011-05-01 Published:2011-05-01

PDF

摘要： 为了方便证明程序的正确性,引入了Kripke结构,提出基于Kripke结构的程序正确性证明。重新定义了适合证明的Kripke结构,并描述了将程序流程图转换为Kripke结构状态图的方法。给出了证明程序正确性的相关定理和基于Kripke结构的程序正确性证明方法。证明方法为:首先,把程序流程图转换为状态图;然后,根据状态之间的转移关系列出每个状态下的状态谓词;最后,证明每个状态谓词为真。根据状态谓词进行证明,能够反映出程序执行的状态。用该方法对一个实例进行了完整的证明。

关键词: Kripke结构, 程序正确性证明, 状态图, 谓词

Abstract: In order to prove program correctness conveniently, Kripke structure was introduced to propose the proof of program correctness. Kripke structure was redefined to be adequate for proof, and the approach of converting program flow chart to Kripke structure state diagram was described. The related theories of proof of program correctness and the method of proof of program correctness based on Kripke structure were also given. First the program flow chart was converted to state diagram, and then the state predicate in every state was listed according to the transformational relation between states. Finally, every state predicate was proved to be true. Proof through the state predicates can reflect the state of program execution. A whole proving process was carried out through an example.

Key words: Kripke structure, proof of program correctness, state diagram, predicate

版权所有 © 2021 四川计算机应用杂志社有限公司
蜀ICP备 05010208 号-3　新出网证(川)字026号
技术支持：北京玛格泰克科技发展有限公司
访问总数：
今日访问：