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
