PVS Specification and Verification System
Dave Stringer-Calvert
Email: dave_sc@csl.sri.com

User Group Presentation

PAMELA+PVS

Bettina Buth,
University of Bremen
bb@informatik.uni-bremen.de

Background

The system PAMELA (Proof Assistant for Meta IV-like Languages) is designed to provide a uniform approach for the formal verification of sequential software. This includes VDM specifications and non-deterministic sequential programs as well as assembler routines, occam procedures, and C modules. The system itself is still in a prototype phase that allows to incorporate changes as they become necessary. The general idea is to calculate proof obligations which ensure overall correctness of the software and discharge these obligations using a suitable basis of rules and lemmas related to the data types used. For this purpose the software has to be given as explicit specifications, i.e. a set of function and procedure definitions and the correctness conditions (usually functional ones) have to be stated as implicit specifications in the form of pre- and postconditions. The generation of obligations is based on the calculation of "relative strongest postconditions" (see [1] for details).

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.

Motivation

The original proof component was developed by the author and strongly influenced by case studies (see [1] for details). It was based on equational reasoning using conditional rewrite rules and deduction rules which formalized the information about datatypes and primitive operators used in the specification. In order to make automatic proofs and the evaluation of proof scripts in the case of failing proofs feasible, a primitive concept of strategies was introduced as well as a number of special treatments e.g. for commutative and associative operators. Although this approach was very successful for the examples considered it has a number of drawbacks:

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 obvious solution for these deficiencies was to substitute the original simple proof component by a full proof system. In order to emulate the ideas implemented in the PAMELA proof component, the system has to fulfill the following criteria:

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.

These criteria are met by PVS and a number of other high-level proof systems as e.g. HOL or Isabel. The previous acquaintance of the author with PVS led to the final choice.

The Interface

The interface between PAMELA and PVS is implemented as a set of Tcl/Tk applications grouped into two windows. This choice of interface is motivated by the different nature of the two systems. PAMELA is a file oriented, non-interactive system implemented in C and running in UNIX shells. Interaction is restricted to reactions to failing proofs and output reflecting the status of the generation of obligations and proofs. PVS on the other side is implemented in LISP and running as an interactive system in an Emacs-environment.

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)