Issue No. 03 - Sept. (1975 vol. 1)
Sanat K. Basu , Department of Computer Sciences, University of Texas at Austin, Austin, Tex. 78712
Raymond T. Yeh , Department of Computer Sciences, University of Texas at Austin, Austin, Tex. 78712
In this paper we investigate the strong verification of programs using the concept of predicate transformer introduced by Dijkstra . We show that every do-while program has a loop invariant that is both necessary and sufficient for proving strong verification. This loop invariant is shown to be the least flxpoint of a recursive function mapping predicates to predicates that is defined by the program and a postcondition.
Silicon, Semantics, Vectors, Computers, Contracts, Indexes, Extrapolation, weakest precondition, Consistency, fixpoint, loop invariant, Q-adequate, strong verification, termination
Sanat K. Basu, Raymond T. Yeh, "Strong verification of programs", IEEE Transactions on Software Engineering, vol. 1, no. , pp. 339-346, Sept. 1975, doi:10.1109/TSE.1975.6312858