Title :
Strong verification of programs
Author :
Basu, Sanat K. ; Yeh, Raymond T.
Author_Institution :
Dept. of Computer Sci., Univ. of Texas, Austin, TX, USA
Abstract :
The authors investigate the strong verification of programs using the concept of predicate transformer introduced by Dijkstra (1974). They show that every do-while program has a loop invariant that is both necessary and sufficient proving strong verification. This loop invariant is shown to be the least fixpoint of a recursive function mapping predicates to predicates that is defined by the program and the postcondition.
Keywords :
programming; consistency; fixpoint; loop invariant; predicate transformer; programs; strong verification; termination; Computers; Contracts; Extrapolation; Indexes; Semantics; Silicon; Vectors; Consistency; Q-adequate; fixpoint; loop invariant; strong verification; termination; weakest precondition;
Journal_Title :
Software Engineering, IEEE Transactions on
DOI :
10.1109/TSE.1975.6312858
