The Community for Technology Leaders
RSS Icon
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
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.
Silicon, Semantics, Vectors, Computers, Contracts, Indexes, Extrapolation, weakest precondition, Consistency, fixpoint, loop invariant, Q-adequate, strong verification, termination
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
13 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool