Weak second order characterizations of various program verification systems (Q1124311)

Program verification systems like the inductive assertions method by Floyd-Hoare, the intermittent assertions method due to Burstall and the temporal logic of programs attributed to Pnueli are revisited to be compared in verification power by Leivant's characterization based on weak second order logic. Leivant's characterization of the Floyd-Hoare logic is proven equivalent to Csirmaz's and Sain's applying Nonstandard Logics of Programs. Then Burstell's and Pnueli's verification systems are subjected to Leivant's weak second order logic as well. Thus all systems presented yield characteristic results in reference to the essential comprehension scheme in weak second order logic. To compare the program verifying powers of different systems one may determine a class of program assertions like partial correctness, total correctness, safety or liveness properties by their first order approximations. To refine this characterization the authors set out to vary the first order approximation to the partial correctness assertion the way pursued by Leivant but from a different starting point. Thus they conclude that Leivant's theorem merely states the equivalence of the Floyd-Hoare method to weak second order program verification with a specific comprehension scheme and a specific weak second order approximation of the partial correctness assertion.