The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.03 - Sept. (1975 vol.1)
pp: 339-346
Raymond T. Yeh , Department of Computer Sciences, University of Texas at Austin, Austin, Tex. 78712
ABSTRACT
In this paper we investigate the strong verification of programs using the concept of predicate transformer introduced by Dijkstra [2]. 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.
INDEX TERMS
Silicon, Semantics, Vectors, Computers, Contracts, Indexes, Extrapolation, weakest precondition, Consistency, fixpoint, loop invariant, Q-adequate, strong verification, termination
CITATION
Raymond T. Yeh, "Strong verification of programs", IEEE Transactions on Software Engineering, vol.1, no. 3, pp. 339-346, Sept. 1975, doi:10.1109/TSE.1975.6312858
70 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool