Title :
Program correctness: on inductive assertion methods
Author_Institution :
IBM Research
Abstract :
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.
Keywords :
Correctness assertions; predicate transformers; program correctness; program proofs; relational semantics; subgoal induction; weakest preconditions; Artificial intelligence; Computer languages; Displays; Induction generators; Terminology; Transformers; Correctness assertions; predicate transformers; program correctness; program proofs; relational semantics; subgoal induction; weakest preconditions;
Journal_Title :
Software Engineering, IEEE Transactions on
DOI :
10.1109/TSE.1980.230787
