Predicate Transformation as a Proof Strategy

In: Erik Polled., Proc. 4th ECOOP Workshop: Formal Techniques for Java-like Programs, Technical Report NIII-R0204. p. 117--128, 2002

Authors

• Nicole Rauch
• Arnd Poetzsch-Heffter

Abstract

In this paper, a verification strategy implementing precondition generation is presented. It automatically constructs a weak precondition for the statements of a Java subset. The strategy uses the rules of an underlying Hoare logic.

Full Text

• PDF: ftfjp02.pdf
• PS.GZ: ftfjp02.ps.gz

BibTeX

@InProceedings{Rauch.Poetzsch-Heffter02predicate, 
   author = {Nicole Rauch and Arnd Poetzsch-Heffter}
   title = {Predicate Transformation as a Proof Strategy },
   booktitle = {Proc. 4th ECOOP Workshop: Formal Techniques for Java-like Programs, Technical Report NIII-R0204},
   organization = {Computing Science Department, University of Nijmegen},
   pages = {117--128},
   year = {2002},
}