A synthesizer of inductive assertions
- 1 March 1975
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Software Engineering
- Vol. SE-1 (1) , 68-75
- https://doi.org/10.1109/tse.1975.6312821
Abstract
Describes a prototype system Vista which provides assistance in synthesizing correct inductive assertions. Given only the source program, it is able to generate a useful class of assertions automatically. For a larger class, it is able to extend partial inductive assertions supplied by the programmer to form complete assertions from which it proves program correctness. Its synthesis methods include: symbolic evaluation in a weak interpretation, combining output assertions with loop exit information to obtain trail loop assertions, and extracting information from proofs which fail in order to determine how assertions should be strengthened.Keywords
This publication has 0 references indexed in Scilit: