This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Program Correctness: On Inductive Assertion Methods
September 1980 (vol. 6 no. 5)
pp. 465-479
J.C. King, IBM Research
A study of several of the proof of correctness methods is presented. In particular, the form of induction used is explored in detail. A relational semantic model for programming languages is introduced and its relation to predicate transformers is explored. A rather elementary viewpoint is taken in order to expose, as simply as possible, the basic differences of the methods and the underlying principles involved. These results were obtained by attempting to thoroughly understand the "subgoal induction" method.
Index Terms:
weakest preconditions, Correctness assertions, predicate transformers, program correctness, program proofs, relational semantics, subgoal induction
Citation:
J.C. King, "Program Correctness: On Inductive Assertion Methods," IEEE Transactions on Software Engineering, vol. 6, no. 5, pp. 465-479, Sept. 1980, doi:10.1109/TSE.1980.230787
Usage of this product signifies your acceptance of the Terms of Use.