Proof of program correctness based on Kripke structure
Yu Jiankun · Journal of Computer Applications · 2011
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.