A User-interface for Proofs and Certified Software
by Janet Bertot, Yves Bertot, Yann Coscoy, Healfdene Goguen and Francis
Montagnac
By making it possible to express the properties of procedures and
functions, proofs assistants can be used to help develop certified software.
However, these proof assistants are often complicated to use and deserve
real user-interfaces to make software development feasible. Since 1990,
The CROAP team at INRIA Sophia-Antipolis has been studying the development
of user-interfaces for theorem provers to reduce this level of complication.
We have implemented a powerful prototype, CtCoq, that has been used successfully
in the development of certified algorithms for program manipulation or
polynomial mathematics. The last version of this proof environment has
been released in February 1997.
The semantics of programs can be mathematically described using relations
between inputs and outputs or using functions from the domain of inputs
to the domain of outputs. When these relations and functions are formally
described, it is possible to use a computer to check mechanically some
of their properties. This leads to the perspective of checking that programs
fulfil a formal specification and ultimately to zero-default software.
Since the correction of a given program may rely on an arbitrarily complex
corpus of mathematics, the system used for the verification needs to have
very powerful proving capabilities. To date, only the systems known as
theorem provers or proof checkers provide enough mathematical capabilities
for this task.
The Coq proof assistant is one such proof checker (see previous article).
It uses type theory to express the properties of functions and encode powerful
mathematical tools such as recursion and algebraic structures. Intuitively,
the types used in a programming language like Pascal or C make it possible
to verify simple consistency properties between the components of a software.
When using language with more expressive types, the properties that can
be expressed using types can actually cover the complete specification
of a software system.
The CtCoq user-interface is an independent front-end for the Coq proof
assistant. It uses technologies from the domain of programming environments
to help the proof developer in several ways.
The first element taken from programming environment technology is the
use of syntax directed tools. These tools use a precise description of
the proof assistant's syntax to help in the rapid construction of syntactically
correct logical sentences, specifications, and proof commands. For instance,
syntax directed menus make it possible to perform transformations on expressions
or commands that respect the syntactic correctness of these expressions,
thus reducing the time spent in correcting low-level errors. Syntax aware
tools also make it easier to recognize usual mathematical notations and
render them using multiple-font display, in a wysiwyg fashion.
These tools make semantic manipulation of data possible, with interpretation
of the user's pointing or dragging gestures using the mouse. For instance,
pointing at an expression can be interpreted guiding the proof process
towards this expression. In the same realm, dragging an expression can
be used to rearrange data when the algebraic properties make it possible.
Other tools taken from programming environments use the analysis of
dependence graphs between functions, mathematical objects, and proof commands.
This analysis can lead to quicker tools to help finding and correcting
errors in specifications, thus making the development of completely proved
software quicker.
Powerful analyses also make it possible to extract natural language
presentation from proofs data structures, thus making the results of proof
developments understandable by mathematicians and engineers outside the
community of Coq and CtCoq users.
The CtCoq proof environment has been used successfully in the development
of algorithms for symbolic computation, trajectory planning, and program
partial evaluation.
Future research around this user-interface aims on one side at a better
integration with symbolic computation and computer algebra systems and
on the other side at a better use of dependency graphs to make large proof
maintenance and re-engineering feasible.
Publication references for this research can be found at: http://www.inria.fr/croap/publications.html
The CtCoq system can be retrieved by following the instructions found
at: http://www.inria.fr/ctcoq/ctcoq-eng.html
Please contact:
Yves Bertot - INRIA
Tel: +33 4 9365 7739
E-mail: Yves.Bertot@inria.fr
