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
