Using a Program Verification Calculus for Constructing Specifications from Implementations

Abstract

In this paper we examine the possibility of automatically constructing the program specification from an implementation, both from a theoretical perspective and as a practical approach with a sequent calculus. As a setting for program specifications we choose dynamic logic for the Java programming language. We show that -- despite the undecidable nature of program analysis -- the strongest specification of any program can always be constructed algorithmically. Further we outline a practical approach embedded into a sequent calculus for dynamic logic and with a higher focus on readability. Therefor, the central aspect of describing unbounded state changes incorporates the concept of modifies lists for expressing the modifiable portion of the state space. The underlying deductions are carried out by the theorem prover of the KeY System.

This work shows how program verification calculi can be used for computing specifications or specification extraction, i.e., for extracting specifications from implementations. It has been implemented as part of the KeY System.

Contents

• PS-Version of this document
• PDF-Version of this document
• Slides from 2nd Swedish-German KeY Workshop, 2003

[Pla04a]

André Platzer (2004). Using a Program Verification Calculus for Constructing Specifications from Implementations. Minor Thesis, University of Karlsruhe, Department of Computer Science. Institute for Logic, Complexity and Deduction Systems, February 2004.
[pdf]

BibTeX

@report{Platzer_2004,
  author       = {Platzer, Andr\'e},
  title        = {Using a Program Verification Calculus for
                  Constructing Specifications from Implementations},
  school       = {University of Karlsruhe, Department of Computer Science.
                  Institute for Logic, Complexity and Deduction Systems},
  howpublished = {Minor Thesis,
                  University of Karlsruhe, Department of Computer Science.
                  Institute for Logic, Complexity and Deduction Systems},
  month        = {February},
  year         = {2004},
}