PROVING THE TOTAL CORRECTNESS OF THE LOOP PROGRAM WITH THE INTERMITTENT-ASSERTION METHOD OVER MULTISET ORDERINGS
Bolin Tang · Computer Applications and Software · 1985
The intermittent-assertion method is a strong technique for proving the total correctness of programs.With to prove programs with it,we must affix intermittent assertions to some of the program's internal key points and supply lemmas to relate these assertions.The proofs of these lemmas involved often complete induction over a well-founded ording.This paper introduces the multiset orderings over a well-founded set.With the multiset orderings,not only the termination functions of lcop program can be easily found,but also its total correctness can be simply and intuitively proved.