Dave Stringer-Calvert

Email:
*dave_sc@csl.sri.com*

University of Bremen

bb@informatik.uni-bremen.de

While PAMELA was developed for proving partial correctness of VDM specifications [3], mainly in the area of code generators, further case studies and projects influenced the changes and extensions of the input language as well as the demands for the prover component. The latter was build into the system in an earlier version of PAMELA and is now substituted by PVS.

- The logic supported was restricted to propositional formulas plus a simple form of universal quantification.
- PAMELA did not support the justification of rules. This would give more confidence in the proof, especially if complex rules have to be used.
- Many errors can be detected simply by performing typechecks, but PAMELA did not exploit type information.
- A large number of rules had to be introduced for defining the underlying datatypes. This was done be stating the effect of constructor, selector and recognizer operations for the abstract datatypes. A more compact way of defining these is very desirable.

- The underlying language should be strongly typed and support higher order logic with full quantification.
- Proofs should be performed interactively, but allowing the use of strategies and automatic simplification of basic expressions.
- The system should be able to deal at least with integer arithmetic, a prerequisite for proving realistic codegenerator specifications correct.
- The system should be well-used and come with good support.

The aim was to find a way of generating the proof obligations successively and submitting them to PVS for examination, i.e. typechecking and/or proving. In this way it is possible to get feedback at the earliest possible time. This feedback comprises typecheck error as well as the necessity to introduce further lemmas in order to proceed with the proof. A positive sideeffect is that the separate treatment of single obligations avoids the disadvantages of confronting PVS with a large theory containing all theorems. This usually leads to very unsatisfactory response times for parsing and typechecking and an explosion of the prover state.

With the Tcl/Tk-interface it is now possible to investigate the individual obligations independently from each other after loading the common basic theory which is usually relatively small. Furthermore it is possible to interrupt and postpone the generation of proof obligations in favor of adding new lemmas or in general modifying the basic theory. The interface also allows to store proofs of individual obligations and submit them to PVS with the original or other obligations. For a detailed description of the interface and its implementation see [2].

[1] Bettina Buth: Operation Refinement Proofs for VDM-like Specifications, Dissertation; auch Bericht Nr. 9501 Institut f{\"u}r Informatik und Praktische Mathematik, Christian-Albrechts-Universit{\"a}t Kiel 1995. (see also: http:\\www.informatik.uni-bremen.de/~bb)

[2] Bettina Buth: An interface between pamela and pvs. Technical report, SRI, 1999. (in preparation).

[3] Cliff~B. Jones: Systematic Software Development using VDM, Series in Computer Science. Prentice-Hall International, Second Edition, 1990.

Dave Stringer-Calvert (dave_sc@csl.sri.com)