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

• 作者: 余建坤 林杰
• 来源期刊: 计算机应用
• 学科: 工学
• 关键词: Kripke结构 程序正确性证明 状态图 谓词
• 年，卷（期）: 2011,（5）
• 所属期刊栏目: 典型应用
• 页码范围: 1425-1427
• 分类号: TP311.1
• 字数: 3670字
• 语种: 中文
• DOI: 10.3724/SP.J.1087.2011.01425

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	余建坤	云南财经大学信息学院	37	165	7.0	10.0
2	林杰	云南财经大学信息学院	1	8	1.0	1.0