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

Proof of program correctness based on Kripke structure

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

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.