TITLE: Program verification and development with Isabelle
AUTHORS: Marek A. Bednarczyk (ICS PAS) & Tomasz Borzyszkowski (IM UG)
ABSTRACT:
The purpose of this paper is to report on our experiments in using
Isabelle --- a general purpose theorem prover --- as a tool for
verification and development of software.
The idea of using a theorem prover for software verification/development
becomes feasible when the process of verification/development is
presented as a {\it logical activity}. In our case this is achieved as
follows.
* At the top level is a logic, called pLSD, which is a Labelled Deductive
System with the following features:
- Declarative units (judgements) of pLSD have form P : A where
P is a program and A is a specification;
- Consequece ||- is tarskian:
p_1 : A_1, ..., p_n : A_n ||- P(p_1,...,p_n) : A
- Labels are programs built from assignments, x := e, and indeterminate
programs, p, and composed with sequential composition, conditional
composition and while loop;
- Specifications are formulae of predicate logic with explicit
substitutions.
- To every programming construct there is a logical rule which
introduces it. For instance, the assignment axiom and the sequential
composition rule look as follows:
_______________________ assignment
||- x := e : [e/x]
Gamma ||- P_1 : A_1 Gamma ||- P_2 : A_2
_______________________________________________ sequent.comp
Gamma ||- P_1;P_2 : A_1 >< A_2
* Specification logic is a non-commutative intuitionistic substructural
theory with sequents of the form: A_1, ..., A_n |- A. The logic
comprises additive conjunction and disjunction and multiplicative
conjunction ><, together with their units. There are two sorts of
atomic formulae: predicates (including `=') and substitutions.
The two consequence relations, i.e., ||- and |-, interact via
consequence rule:
p_1 : A_1, ..., p_n : A_n ||- P(p_1,...,p_n) : A B |- A
____________________________________________________________
p_1 : A_1, ..., p_n : A_n ||- P(p_1,...,p_n) : B
* The substructural theory contains a `classical theory' which describes
properties of the domain of objects manipulated by programs. This is
described at the level of usual predicate logic with equality. The
substructural theory is a conservative extension of the classical.
Thus, in an attempt to code pLSD in Isabelle, we are led to define
3 logics - one on top of another.
- The most general is ||-, i.e., pLSD.
- Program verification/development in pLSD generates proof obligations
of the form A |- B, i.e., at the level of specification logic;
- Finally, elimination of substitutions from specification sequents
generates proofs at the level of the basic theory.
We plan to show how, with our encoding, one can formally develop a program
which satisfies a given specification. The example should also demonstrate
shortcommings of our encoding.