DocumentCode
1297616
Title
Strong verification of programs
Author
Basu, Sanat K. ; Yeh, Raymond T.
Author_Institution
Dept. of Computer Sci., Univ. of Texas, Austin, TX, USA
Issue
3
fYear
1975
Firstpage
339
Lastpage
346
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;
fLanguage
English
Journal_Title
Software Engineering, IEEE Transactions on
Publisher
ieee
ISSN
0098-5589
Type
jour
DOI
10.1109/TSE.1975.6312858
Filename
6312858
Link To Document