Using a program verification calculus for constructing specifications from implementations

In this thesis 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.