This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Strong verification of programs
Sept. 1975 (vol. 1 no. 3)
pp. 339-346
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 [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:
Sanat K. Basu, 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
Usage of this product signifies your acceptance of the Terms of Use.