At present, most tools for correct programming support functional or logical
programming paradigms. However, in practice, most programs are written using
procedural languages (including object-oriented languages) like Pascal, C/C++
or Java. Tools for procedural languages usually provide only syntactical
support.
The essence of algorithms in procedural languages can be expressed in
Dijkstra's guarded command language (GCL), for which there is a formal basis
that allows semantical support. In fact, programs written in GCL can be
derived from their specification, as is shown in [Dij76,Kal90].
So far, there are only few tools that support this approach
to programming.
The goal of Cocktail is to provide semantical support for deriving programs
from their specifications. The system is intended for programmers in an
educational setting. Cocktail is mainly practice-oriented to increase its
usability for the intended users. Also, the system is set up to be extensible,
flexible and easy to experiment with.
Cocktail is written entirely in Java and provides a modern graphical user
interface. Proofs are graphically represented in Fitch-style natural deduction
and can be manipulated by drag-and-drop operations.
Forward reasoning is supported to a certain extend, allowing the user more
flexibility than backward reasoning only.
Logical foundation
To ensure a firm logical foundation of the system, we use a typed lambda
calculus for the logical parts of our system. Typed lambda calculi are
suitable for interactive theorem proving, as is shown by systems like
Coq,
LEGO
and Yarrow
. Instead of using a fixed calculus, we use a logical framework of typed
lambda calculi: the framework of Pure Type Systems (PTSs). This approach has
several advantages. Firstly, it allows us to easily increase the expressive
power of the logical foundation of the system at a later stage, without
having to re-implement the entire logic. Secondly, we can use a type checking
algorithm to verify the correctness of constructed proofs, thereby avoiding
errors being introduced when the theorem prover gets large. Thirdly, we can
communicate our proofs to other proof systems, since lambda terms are
standardized proof objects.
On the other hand, typed lambda calculi are usually used for higher order
logics, which are not (yet) needed for our system. During the derivation of
a program, many first-order theorems have to be proved, most of which are
relatively simple. Since for first order theorems good automation is possible,
it is desirable to include an automated theorem prover (ATP) in the system.
However, ATPs are usually based on other formalisms and use other techniques
to prove theorems than interactive theorem provers.
Embedding First-Order Tableaux in a Pure Type System
In Cocktail, automated and interactive theorem proving are combined as
follows: Firstly, an extension, introduced in [Laa97], to the standard PTSs is
used to faithfully model first order logic. Secondly, a tableaux based
theorem prover is implemented that directly uses the formulas from the
extended PTS. Since we use a faithful model of first order logic, no problems
will occur during the construction of the semantic tableau. Thirdly, the
tableau constructed by the ATP is translated into a lambda-term of the
underlying logic. A precise description of the translation algorithm and the
resulting system can be found in this report
(postscript).
Linking Hoare Logic with a Pure Type System
In the Hoare logic or axiomatic semantics of the guarded command language
supported by Cocktail, programs are annotated with proofs and specifications.
The proofs in the annotation provide enough information to check a posteriori
if a constructed program does indeed meet its specification. Just as a simple
type checking algorithm can ensure that a constructed proof (lambda-term) is
correct, a simple program checking algorithm ensures an annotated program is
correct. In this way the soundness of Cocktail depends only on this checking
algorithm, and not on the whole system, which may get quite large.
Result
Cocktail is an experimental system for deriving correct programs, aimed at
students. The underlying logic can easily be extended and changed, since a
logical framework is used rather than a fixed logic. Many of the simple
theorems are proved automatically. The graphical user interface provides a
clear view of the proofs and allows intuitive construction of proofs.
