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.