ERCIM News No.36 - January 1999

Certification of Imperative Programs in the System Coq

by Jean-Christophe Filliâtre

---

The system Coq is a proof assistant developed by the Coq team at INRIA, so far used to formalize mathematics and to prove the correctness of purely functional programs. From now on, it may also be used to establish the correctness and the termination of imperative programs (in fragments of C, Pascal, or ML).

The Coq Proof Assistant (see ERCIM News number 32) is a tool for specification and formal proofs, based on a highly expressive logic, the Calculus of Inductive Constructions. Therefore, it is naturally suited for mathematical formalizations and proofs of purely functional programs, since those are already terms of the logic. But the certification of programs is not realistic without dealing also with imperative programs, so a module of certification of imperative programs has been recently introduced in the system Coq.

The programs are given in an ML-Pascal dialect mixing imperative features (references, arrays, while loops, sequences) and functional features (functions as first-order objects, polymorphism, recursive datatypes). They are specified in a Floyd-Hoare logic style, by insertion of logical assertions, such as pre- or post-conditions or loop invariants. Termination is justified by the insertion of a pair variant/relation associated to each loop or recursive function. Then an automatic tactic takes a specified program and produces some proof obligations, whose validity implies both correctness and termination of the initial program.

The method involved is based on a functional translation of imperative programs. Starting with an annotated program, we first determine its effects (access or modification of references or arrays). Then, using this information, we build a proof of its specification, whose skeleton is a functional translation of the imperative program which expresses its semantics. This proof is of course incomplete, and each ‘hole’ will correspond to a proof obligation. Indeed, this partial proof term is given to a specific tactic which proves the specification by generating a proof obligation for each missing part of the proof term, in a way similar to the type-checking conditions (TCC) of the PVS system. It is important to notice that this functional translation, and the corresponding proof term, are completely hidden. The user only sees the specified program he gave, and the resulting proof obligations. Then he can use all the power of the proof assistant to prove them. Once the proofs are done, the programs can be pretty-printed in C or ML code to be compiled and linked in bigger applications.

This technology is already distributed with the system Coq, and has been applied on quite complex algorithms (select, quick sorting algorithms, Knuth-Morris-Pratt string searching, ...). The interests of such an approach are mainly the use of a highly expressive logic and the use of a secure proof assistant with a great experience in formal proofs.

There is still some work to be done to reach a fully operational certification environment for imperative programs. A first improvement will be an extension of the programming language, with an addition of exceptions and other imperative datatypes such as records for instance. Another improvement, which is essential, concerns modularity, since there is no big software development without a good notion of modules. So we have to understand what is a good notion of module with respect to specified programs, and in particular what are the visibility rules associated to those modules.

For more information about the Coq project and the certification of imperative programs in the system Coq, see web site: http://coq.inria.fr/

Please contact:

Jean-Christophe Filliâtre - INRIA
Tel: +33 1 69 15 64 53
E-mail: Jean-Christophe.Filliatre@inria.fr