Proving total correctness of nondeterministic programs in infinitary logic : (preprint)
R. J. R. Back · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1980
It is shown how the weakest precondition approach to proving total correctness of nondeterministic programs can be formalized in infinitary logic.The weakest precondition technique is extended to hierarchically structured programs by adding a new primitive statement for operational abstraction, the nondeterministic assignment statement, to the guarded commands of Dijkstra.The infinitary logic Lwiw is shown to be strong enough to express the weakest preconditions for Dijkstra's guarded commands, but too weak for the extended guarded commands.Two possible solutions are considered: going to the essentially stronger infinitary logic Lw w and restricting the power of the nondeterministic assignment statemen!ln a way which allows the weakest preconditions to be expressed in Lwiw•