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.