documentation automatique de la biblio standard

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8188 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 928 insertions, 0 deletions

diff --git a/doc/Correctness.tex b/doc/Correctness.tex
new file mode 100644
index 000000000..1b24207f6
--- /dev/null
+++ b/doc/Correctness.tex
@@ -0,0 +1,928 @@
+\achapter{Proof of imperative programs}
+\aauthor{Jean-Christophe Filliâtre}
+\label{Addoc-programs}
+\index{Imperative programs!proof of}
+\comindex{Correctness}
+
+%%%%%%%%%%%%%%%%
+% Introduction %
+%%%%%%%%%%%%%%%%
+
+This chapter describes a new tactic
+to prove the correctness and termination of imperative
+programs annotated in a Floyd-Hoare logic style.
+The theoretical fundations of this tactic are described 
+in~\cite{Filliatre99,Filliatre00a}.
+This tactic is provided in the \Coq\ module \texttt{Correctness},
+which does not belong to the initial state of \Coq. So you must import
+it when necessary, with the following command:
+$$
+\mbox{\texttt{Require Correctness.}}
+$$
+
+
+%%%%%%%%%%%%%%%%%%%%%
+% comment ça marche %
+%%%%%%%%%%%%%%%%%%%%%
+
+\asection{How it works}
+
+Before going on into details and syntax, let us give a quick overview
+of how that tactic works. 
+Its behavior is the following: you give a
+program annotated with logical assertions and the tactic will generate
+a bundle of subgoals, called \emph{proof obligations}. Then, if you
+prove all those proof obligations, you will establish the correctness and the
+termination of the program.
+The implementation currently supports traditional imperative programs
+with references and arrays on arbitrary purely functional datatypes,
+local variables, functions with call-by-value and call-by-variable
+arguments, and recursive functions.
+
+Although it behaves as an implementation of Floyd-Hoare logic, it is not.
+The idea of the underlying mechanism is to translate the imperative
+program into a partial proof of a proposition of the kind
+$$
+\forall \vec{x}. P(\vec{x}) 
+  \Rightarrow \exists(\vec{y},v). Q(\vec{x},\vec{y},v)
+$$
+where $P$ and $Q$ stand for the pre- and post-conditions of the
+program, $\vec{x}$ and $\vec{y}$ the variables used and modified by
+the program and $v$ its result.
+Then this partial proof is given to the tactic \texttt{Refine}
+(see~\ref{Refine}, page~\pageref{Refine}), which effect is to generate as many
+subgoals as holes in the partial proof term.
+
+\medskip
+
+The syntax to invoke the tactic is the following:
+$$
+\mbox{\tt Correctness} ~~ ident ~~ annotated\_program.
+$$
+Notice that this is not exactly a \emph{tactic}, since it does not
+apply to a goal. To be more rigorous, it is the combination of a
+vernacular command (which creates the goal from the annotated program)
+and a tactic (which partially solves it, leaving some proof
+obligations to the user).
+
+Although \texttt{Correctness} is not a tactic, the following syntax is
+available:  
+$$
+\mbox{\tt Correctness} ~~ ident ~~ annotated\_program ~ ; ~ tactic.
+$$
+In that case, the given tactic is applied on any proof
+obligation generated by the first command.
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Syntaxe de programmes annotes %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\asection{Syntax of annotated programs}
+
+\asubsection{Programs}
+
+The syntax of programs is given in figure~\ref{fig:ProgramsSyntax}.
+Basically, the programming language is a purely functional kernel
+with an addition of references and arrays on purely functional values.
+If you do not consider the logical assertions, the syntax coincide
+with \ocaml\ syntax, except for elements of arrays which are written
+$t[i]$. In particular, the dereference of a mutable variable $x$ is
+written $!x$ and assignment is written \verb!:=!
+(for instance, the increment of the variable $x$ will
+be written \verb@x := !x + 1@).
+Actually, that syntax does not really matters, since it would
+be extracted later to real concrete syntax, in different programming
+languages. 
+
+\begin{figure}[htbp]
+  \begin{center}
+    \leavevmode
+$$
+\begin{array}{lrl}
+    prog & ::= & \verb!{! ~ predicate ~ \verb!}! *
+                 ~ statement ~ [ \verb!{! ~ predicate ~ \verb!}! ] \\
+
+    & & \\[0.1em]
+
+    statement
+         & ::= & expression \\
+         &   | & identifier ~ \verb!:=! ~ prog \\
+         &   | & identifier ~ \verb![! ~ expression ~ \verb!]!
+                 ~ \verb!:=! ~ prog \\
+         &   | & \verb!let! ~ identifier ~ \verb!=! ~ \verb!ref! ~
+                  prog ~ \verb!in! ~ prog \\
+         &   | & \verb!if! ~ prog ~ \verb!then! ~ prog 
+                 ~ [ \verb!else! ~ prog ] \\
+         &   | & \verb!while! ~ prog ~ \verb!do! 
+                 ~ loop\_annot ~ block ~ \verb!done! \\
+         &   | & \verb!begin! ~ block ~ \verb!end! \\
+         &   | & \verb!let! ~ identifier ~ \verb!=! ~ prog ~ 
+                 \verb!in! ~ prog \\
+         &   | & \verb!fun! ~ binders ~ \verb!->! ~ prog \\
+         &   | & \verb!let! ~ \verb!rec! ~ identifier ~ binder ~ \verb!:! 
+                 ~ value\_type \\
+         &     & ~~ \verb!{! ~ \verb!variant! ~ wf\_arg ~ \verb!}! 
+                 ~ \verb!=! ~ prog ~ [ \verb!in! ~ prog ] \\
+         &   | & \verb!(! ~ prog ~~ prog ~ \verb!)! \\
+
+    & & \\[1em]
+
+    expression
+         & ::= & identifier \\
+         &   | & \verb@!@ ~ identifier \\
+         &   | & identifier ~ \verb![! ~ expression ~ \verb!]! \\
+         &   | & integer \\
+         &   | & \verb!(! ~ expression+  \verb!)! \\
+
+    & & \\[1em]
+
+    block & ::= & block\_statement ~ [ ~ \verb!;! ~ block ~ ] \\
+
+    & & \\[0.1em]
+
+    block\_statement
+          & ::= & prog \\
+          &   | & \verb!label! ~ identifier \\
+          &   | & \verb!assert! ~ \verb!{! ~ predicate ~ \verb!}! \\
+
+    & & \\[1em]
+
+    binders & ::= & \verb!(! ~ identifier,\dots,identifier ~ \verb!:!
+                    ~ value\_type ~ \verb!)! + \\
+
+    & & \\[1em]
+
+    loop\_annot 
+          & ::= & \verb!{! ~ \verb!invariant! ~ predicate ~
+                  \verb!variant! ~ wf\_arg ~ \verb!}! \\
+    & & \\[0.1em]
+
+    wf\_arg & ::= & cic\_term ~ [ \verb!for! ~ cic\_term ] \\
+
+    & & \\[0.1em]
+
+    predicate & ::= & cci\_term ~ [ \verb!as! ~ identifier ] \\
+
+  \end{array}
+$$
+      \caption{Syntax of annotated programs}
+    \label{fig:ProgramsSyntax}
+  \end{center}
+\end{figure}
+
+
+\paragraph{Syntactic sugar.}
+
+\begin{itemize}
+  \item \textbf{Boolean expressions:} 
+
+    Boolean expressions appearing in programs (and in particular in
+    \kw{if} and \kw{while} tests) are arbitrary programs of type \texttt{bool}.
+    In order to make programs more readable, some syntactic sugar is
+    provided for the usual logical connectives and the usual order
+    relations over type \texttt{Z}, with the following syntax:
+    $$
+    \begin{array}{lrl}
+      prog
+      & ::= & prog ~ \verb!and! ~ prog \\
+      &   | & prog ~ \verb!or!  ~ prog \\
+      &   | & \verb!not! ~ prog \\
+      &   | & expression ~ order\_relation ~ expression \\[1em]
+      order\_relation
+      & ::= & \verb!>! ~|~ \verb!>=! ~|~ \verb!<! ~|~ \verb!<=! 
+      ~|~ \verb!=! ~|~ \verb!<>! \\
+    \end{array}
+    $$
+    where the order relations have the strongest precedences,
+    \verb!not! has a stronger precedence than \verb!and!,
+    and \verb!and! a stronger precedence than \verb!or!.
+    
+    Order relations in other types, like \texttt{lt}, \texttt{le}, \dots in
+    type \texttt{nat}, should be explicited as described in the
+    paragraph about \emph{Boolean expressions}, page~\pageref{prog:booleans}.
+
+  \item \textbf{Arithmetical expressions:}
+
+    Some syntactic sugar is provided for the usual arithmetic operator
+    over type \texttt{Z}, with the following syntax:
+    $$
+    \begin{array}{lrl}
+      prog
+      & ::= & prog ~ \verb!*! ~ prog \\
+      &   | & prog ~ \verb!+! ~ prog \\
+      &   | & prog ~ \verb!-! ~ prog \\
+      &   | & \verb!-! ~ prog 
+    \end{array}
+    $$
+    where the unary operator \texttt{-} has the strongest precedence,
+    and \texttt{*} a stronger precedence than \texttt{+} and \texttt{-}.
+
+    Operations in other arithmetical types (such as type \texttt{nat})
+    must be explicitly written as applications, like 
+    \texttt{(plus~a~b)}, \texttt{(pred~a)}, etc.
+
+  \item \texttt{if $b$ then $p$} is a shortcut for
+    \texttt{if $b$ then $p$ else tt}, where \texttt{tt} is the
+    constant of type \texttt{unit};
+
+  \item Values in type \texttt{Z}
+    may be directly written as integers : 0,1,12546,\dots
+    Negative integers are not recognized and must be written
+    as \texttt{(Zinv $x$)};
+
+  \item Multiple application may be written $(f~a_1~\dots~a_n)$,
+    which must be understood as left-associa\-tive
+    i.e. as $(\dots((f~a_1)~a_2)\dots~a_n)$.
+\end{itemize}
+
+
+\paragraph{Restrictions.}
+
+You can notice some restrictions with respect to real ML programs:
+\begin{enumerate}
+  \item Binders in functions (recursive or not) are explicitly typed,
+    and the type of the result of a recursive function is also given.
+    This is due to the lack of type inference.
+
+  \item Full expressions are not allowed on left-hand side of assignment, but
+    only variables. Therefore, you can not write
+\begin{verbatim}
+    (if b then x else y) := 0
+\end{verbatim}
+    But, in most cases, you can rewrite
+    them into acceptable programs. For instance, the previous program
+    may be rewritten into the following one:
+\begin{verbatim}
+    if b then x := 0 else y := 0
+\end{verbatim}
+\end{enumerate}
+
+
+
+%%%%%%%%%%%%%%%
+% Type system %
+%%%%%%%%%%%%%%%
+
+\asubsection{Typing}
+
+The types of annotated programs are split into two kinds: the types of
+\emph{values} and the types of \emph{computations}. Those two types
+families are recursively mutually defined with the following concrete syntax:
+$$
+\begin{array}{lrl}
+  value\_type
+    & ::= & cic\_term \\
+    &   | & {cic\_term} ~ \verb!ref! \\
+    &   | & \verb!array! ~ cic\_term ~ \verb!of! ~ cic\_term \\
+    &   | & \verb!fun! ~ \verb!(! ~ x \verb!:! value\_type ~ \verb!)!\!+
+            ~ computation\_type \\
+    &     & \\
+  computation\_type
+    & ::= & \verb!returns! ~ identifier \verb!:! value\_type \\
+    &     & [\verb!reads! ~ identifier,\ldots,identifier] 
+            ~ [\verb!writes! ~ identifier,\ldots,identifier] \\
+    &     & [\verb!pre! ~ predicate] ~ [\verb!post! ~ predicate] \\
+    &     & \verb!end! \\
+    &     & \\
+  predicate
+    & ::= & cic\_term \\
+    &     & \\
+\end{array}
+$$
+
+The typing is mostly the one of ML, without polymorphism.
+The user should notice that:
+\begin{itemize}
+  \item Arrays are indexed over the type \texttt{Z} of binary integers 
+    (defined in the module \texttt{ZArith});
+
+  \item Expressions must have purely functional types, and can not be 
+    references or arrays (but, of course, you can pass mutables to
+    functions as call-by-variable arguments);
+
+  \item There is no partial application.
+\end{itemize}
+
+
+%%%%%%%%%%%%%%%%%%
+% Specifications %
+%%%%%%%%%%%%%%%%%%
+
+\asubsection{Specification}
+
+The specification part of programs is made of different kind of
+annotations, which are terms of sort \Prop\ in the Calculus of Inductive
+Constructions.
+
+Those annotations can refer to the values of the variables
+directly by their names. \emph{There is no dereference operator ``!'' in
+annotations}. Annotations are read with the \Coq\ parser, so you can
+use all the \Coq\ syntax to write annotations. For instance, if $x$
+and $y$ are references over integers (in type \texttt{Z}), you can write the
+following annotation
+$$
+\mbox{\texttt{\{ `0 < x <= x+y` \}}}
+$$
+In a post-condition, if necessary, you can refer to the value of the variable
+$x$ \emph{before} the evaluation with the notation $x@$.
+Actually, it is possible to refer to the value of a variable at any 
+moment of the evaluation with the notation $x@l$,
+provided that $l$ is a \emph{label} previously inserted in your program
+(see below the paragraph about labels).
+
+You have the possibility to give some names to the annotations, with
+the syntax
+$$
+\texttt{\{ \emph{annotation} as \emph{identifier} \}}
+$$
+and then the annotation will be given this name in the proof
+obligations.
+Otherwise, fresh names are given automatically, of the kind
+\texttt{Post3}, \texttt{Pre12}, \texttt{Test4}, etc.
+You are encouraged to give explicit names, in order not to have to
+modify your proof script when your proof obligations change (for
+instance, if you modify a part of the program).
+
+
+\asubsubsection{Pre- and post-conditions}
+
+Each program, and each of its sub-programs, may be annotated by a
+pre-condition and/or a post-condition.
+The pre-condition is an annotation about the values of variables
+\emph{before} the evaluation, and the post-condition is an annotation
+about the values of variables \emph{before} and \emph{after} the
+evaluation. Example:
+$$
+\mbox{\texttt{\{ `0 < x` \} x := (Zplus !x !x) \{ `x@ < x` \}}}
+$$
+Moreover, you can assert some properties of the result of the evaluation
+in the post-condition, by referring to it through the name \emph{result}.
+Example:
+$$
+\mbox{\texttt{(Zs (Zplus !x !x)) \{ (Zodd result) \}}}
+$$
+
+
+\asubsubsection{Loops invariants and variants}
+
+Loop invariants and variants are introduced just after the \kw{do}
+keyword, with the following syntax:
+$$
+\begin{array}{l}
+  \kw{while} ~ B ~ \kw{do} \\
+  ~~~ \{ ~ \kw{invariant} ~ I ~~~ \kw{variant} ~ \phi ~ \kw{for} ~ R ~
+      \} \\
+  ~~~ block \\
+  \kw{done}
+\end{array}
+$$
+
+The invariant $I$ is an annotation about the values of variables
+when the loop is entered, since $B$ has no side effects ($B$ is a
+purely functional expression). Of course, $I$ may refer to values of
+variables at any moment before the entering of the loop.
+
+The variant $\phi$ must be given in order to establish the termination of
+the loop. The relation $R$ must be a term of type $A\rightarrow
+A\rightarrow\Prop$, where $\phi$ is of type $A$.
+When $R$ is not specified, then $\phi$ is assumed to be of type
+\texttt{Z} and the usual order relation on natural number is used.
+
+
+\asubsubsection{Recursive functions}
+
+The termination of a recursive function is justified in the same way as
+loops, using a variant. This variant is introduced with the following syntax
+$$
+\kw{let} ~ \kw{rec} ~ f ~ (x_1:V_1)\dots(x_n:V_n) : V
+  ~ \{ ~ \kw{variant} ~ \phi ~ \kw{for} ~ R ~ \} = prog
+$$
+and is interpreted as for loops. Of course, the variant may refer to
+the bound variables $x_i$.
+The specification of a recursive function is the one of its body, $prog$.
+Example:
+$$
+\kw{let} ~ \kw{rec} ~ fact ~ (x:Z) : Z ~ \{ ~ \kw{variant} ~ x \} =
+  \{ ~ x\ge0 ~ \} ~ \dots ~ \{ ~ result=x! ~ \}
+$$
+
+
+\asubsubsection{Assertions inside blocks}
+
+Assertions may be inserted inside blocks, with the following syntax
+$$
+\kw{begin} ~ block\_statements \dots; ~ \kw{assert} ~ \{ ~ P ~ \};
+  ~ block\_statements \dots ~ \kw{end}
+$$
+The annotation $P$ may refer to the values of variables at any labels
+known at this moment of evaluation.
+
+
+\asubsubsection{Inserting labels in your program}
+
+In order to refer to the values of variables at any moment of
+evaluation of the program, you may put some \emph{labels} inside your
+programs. Actually, it is only necessary to insert them inside blocks,
+since this is the only place where side effects can appear. The syntax
+to insert a label is the following:
+$$
+\kw{begin} ~ block\_statements \dots; ~ \kw{label} ~ L;
+  ~ block\_statements \dots ~ \kw{end}
+$$
+Then it is possible to refer to the value of the variable $x$ at step
+$L$ with the notation $x@L$.
+
+There is a special label $0$ which is automatically inserted at the
+beginning of the program. Therefore, $x@0$ will always refer to the
+initial value of the variable $x$.
+
+\medskip
+
+Notice that this mechanism allows the user to get rid of the so-called
+\emph{auxiliary variables}, which are usually widely used in
+traditional frameworks to refer to previous values of variables.
+
+
+%%%%%%%%%%%%
+% booléens %
+%%%%%%%%%%%%
+
+\asubsubsection{Boolean expressions}\label{prog:booleans}
+
+As explained above, boolean expressions appearing in \kw{if} and
+\kw{while} tests are arbitrary programs of type \texttt{bool}. 
+Actually, there is a little restriction: a test can not do some side
+effects. 
+Usually, a test if annotated in such a way:
+$$
+  B ~ \{ \myifthenelse{result}{T}{F} \}
+$$
+(The \textsf{if then else} construction in the annotation is the one
+of \Coq\ !)
+Here $T$ and $F$ are the two propositions you want to get in the two
+branches of the test.
+If you do not annotate a test, then $T$ and $F$ automatically become
+$B=\kw{true}$ and $B=\kw{false}$, which is the usual annotation in
+Floyd-Hoare logic.
+
+But you should take advantages of the fact that $T$ and $F$ may be
+arbitrary propositions, or you can even annotate $B$ with any other
+kind of proposition (usually depending on $result$).
+
+As explained in the paragraph about the syntax of boolean expression,
+some syntactic sugar is provided for usual order relations over type
+\texttt{Z}. When you write $\kw{if} ~ x<y ~ \dots$ in your program,
+it is only a shortcut for $\kw{if} ~ (\texttt{Z\_lt\_ge\_bool}~x~y) ~ \dots$,
+where \texttt{Z\_lt\_ge\_bool} is the proof of
+$\forall x,y:\texttt{Z}. \exists b:\texttt{bool}.
+ (\myifthenelse{b}{x<y}{x\ge y})$
+i.e. of a program returning a boolean with the expected post-condition.
+But you can use any other functional expression of such a type.
+In particular, the \texttt{Correctness} standard library comes
+with a bunch of decidability theorems on type \texttt{nat}:
+$$
+\begin{array}{ll}
+  zerop\_bool & : \forall n:\kw{nat}.\exists b:\texttt{bool}.
+    \myifthenelse{b}{n=0}{0<n} \\
+  nat\_eq\_bool & : \forall n,m:\kw{nat}.\exists b:\texttt{bool}.
+    \myifthenelse{b}{n=m}{n\not=m} \\
+  le\_lt\_bool & : \forall n,m:\kw{nat}.\exists b:\texttt{bool}.
+    \myifthenelse{b}{n\le m}{m<n} \\
+  lt\_le\_bool & : \forall n,m:\kw{nat}.\exists b:\texttt{bool}.
+    \myifthenelse{b}{n<m}{m\le n} \\
+\end{array}
+$$
+which you can combine with the logical connectives.
+
+It is often the case that you have a decidability theorem over some
+type, as for instance a theorem of decidability of equality over some
+type $S$:
+$$
+S\_dec : (x,y:S)\sumbool{x=y}{\neg x=y}
+$$
+Then you can build a test function corresponding to $S\_dec$ using the
+operator \texttt{bool\_of\_sumbool} provided with the
+\texttt{Prorgams} module, in such a way:
+$$
+\texttt{Definition} ~ S\_bool ~ \texttt{:=} 
+  [x,y:S](\texttt{bool\_of\_sumbool} ~ ? ~ ? ~ (S\_dec ~ x ~ y))
+$$
+Then you can use the test function $S\_bool$ in your programs,
+and you will get the hypothesis $x=y$ and $\neg x=y$ in the corresponding
+branches. 
+Of course, you can do the same for any function returning some result
+in the constructive sum $\sumbool{A}{B}$.
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% variables locales et globales %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\asection{Local and global variables}
+
+\asubsection{Global variables}
+\comindex{Global Variable}
+
+You can declare a new global variable with the following command
+$$
+\mbox{\texttt{Global Variable}} ~~ x ~ : ~ value\_type.
+$$
+where $x$ may be a reference, an array or a function.
+\Example
+\begin{verbatim}
+Parameter N : Z.
+Global Variable x : Z ref.
+Correctness foo { `x < N` } begin x := (Zmult 2 !x) end { `x < 2*N` }.
+\end{verbatim}
+
+\comindex{Show Programs}
+Each time you complete a correctness proof, the corresponding program is
+added to the programs environment. You can list the current programs
+environment with the command
+$$
+\mbox{\texttt{Show Programs.}}
+$$
+
+
+\asubsection{Local variables}
+
+Local variables are introduced with the following syntax
+$$
+\mbox{\texttt{let}} ~ x ~ = ~ \mbox{\texttt{ref}} ~ e_1 
+~ \mbox{\texttt{in}} ~ e_2
+$$
+where the scope of $x$ is exactly the program $e_2$.
+Notice that, as usual in ML, local variables must be
+initialized (here with $e_1$).
+
+When specifying a program including local variables, you have to take
+care about their scopes. Indeed, the following two programs are not
+annotated in the same way:
+\begin{itemize}
+  \item $\kw{let} ~ x = e_1 ~ \kw{in} ~ e_2 ~ \spec{Q}$ \\
+    The post-condition $Q$ applies to $e_2$, and therefore $x$ may
+    appear in $Q$;
+
+  \item $(\kw{let} ~ x = e_1 ~ \kw{in} ~ e_2) ~ \spec{Q}$ \\
+    The post-condition $Q$ applies to the whole program, and therefore
+    the local variable $x$ may \emph{not} appear in $Q$ (it is beyond
+    its scope).
+\end{itemize}
+
+
+%%%%%%%%%%%%%%%%%
+% Function call %
+%%%%%%%%%%%%%%%%%
+
+\asection{Function call}
+
+Still following the syntax of ML, the function application is written
+$(f ~ a_1 ~ \ldots ~ a_n)$, where $f$ is a function and the $a_i$'s
+its arguments. Notice that $f$ and the $a_i$'s may be annotated
+programs themselves.
+
+In the general case, $f$ is a function already specified (either with
+\texttt{Global Variable} or with a proof of correctness) and has a
+pre-condition $P_f$ and a post-condition $Q_f$.
+
+As expected, a proof obligation is generated, which correspond to
+$P_f$ applied to the values of the arguments, once they are evaluated.
+
+Regarding the post-condition of $f$, there are different possible cases:
+\begin{itemize}
+  \item either you did not annotate the function call, writing directly
+    $$(f ~ a_1 ~ \ldots ~ a_n)$$
+    and then the post-condition of $f$ is added automatically
+    \emph{if possible}: indeed, if some arguments of $f$ make side-effects
+    this is not always possible. In that case, you have to put a 
+    post-condition to the function call by yourself;
+
+  \item or you annotated it with a post-condition, say $Q$:
+    $$(f ~ a_1 ~ \ldots ~ a_n) ~ \spec{Q}$$
+    then you will have to prove that $Q$ holds under the hypothesis that
+    the post-condition $Q_f$ holds (where both are
+    instantiated by the results of the evaluation of the $a_i$). 
+    Of course, if $Q$ is exactly the post-condition of $f$ then
+    the corresponding proof obligation will be automatically
+    discharged.
+\end{itemize}
+
+
+%%%%%%%%%%%%
+% Libraries %
+%%%%%%%%%%%%
+
+\asection{Libraries}
+\index{Imperative programs!libraries}
+
+The tactic comes with some libraries, useful to write programs and
+specifications.
+The first set of libraries is automatically loaded with the module
+\texttt{Correctness}. Among them, you can find the modules:
+\begin{description}
+  \item[ProgWf]: this module defines a family of relations $Zwf$ on type
+    \texttt{Z} by
+    $$(Zwf ~ c) = \lambda x,y. c\le x \land c \le y \land x < y$$
+    and establishes that this relation is well-founded for all $c$
+    (lemma \texttt{Zwf\_well\_founded}). This lemma is automatically
+    used by the tactic \texttt{Correctness} when necessary.
+    When no relation is given for the variant of a loop or a recursive
+    function, then $(Zwf~0)$ is used \emph{i.e.} the usual order
+    relation on positive integers.
+
+  \item[Arrays]: this module defines an abstract type \texttt{array}
+    for arrays, with the corresponding operations \texttt{new},
+    \texttt{access} and \texttt{store}. Access in a array $t$ at index
+    $i$ may be written \texttt{\#$t$[$i$]} in \Coq, and in particular
+    inside specifications.
+    This module also provides some axioms to manipulate arrays
+    expression, among which \texttt{store\_def\_1} and
+    \texttt{store\_def\_2} allow you to simplify expressions of the
+    kind \texttt{(access (store $t$ $i$ $v$) $j$)}.
+\end{description}
+
+\noindent Other useful modules, which are not automatically loaded, are the
+following:
+\begin{description}
+  \item[Exchange]: this module defines a predicate \texttt{(exchange
+      $t$ $t'$ $i$ $j$)} which means that elements of indexes $i$ and
+    $j$ are swapped in arrays $t$ and $t'$, and other left unchanged.
+    This modules also provides some lemmas to establish this property
+    or conversely to get some consequences of this property.
+    
+  \item[Permut]: this module defines the notion of permutation between
+    two arrays, on a segment of the arrays (\texttt{sub\_permut}) or
+    on the whole array (\texttt{permut}). 
+    Permutations are inductively defined as the smallest equivalence
+    relation containing the transpositions (defined in the module
+    \texttt{Exchange}).
+
+  \item[Sorted]: this  module defines the property  for an array to be
+    sorted, on the whole  array  (\texttt{sorted\_array}) or on a  segment
+    (\texttt{sub\_sorted\_array}). It  also   provides  a few   lemmas  to
+    establish this property.
+\end{description}
+
+
+
+%%%%%%%%%%%%%%
+% Extraction %
+%%%%%%%%%%%%%%
+
+\asection{Extraction}
+\index{Imperative programs!extraction of}
+
+Once a program is proved, one usually wants to run it, and that's why
+this implementation comes with an extraction mechanism.
+For the moment, there is only extraction to \ocaml\ code.
+This functionality is provided by the following module:
+$$
+\mbox{\texttt{Require ProgramsExtraction.}}
+$$
+This extraction facility extends the extraction of functional programs
+(see chapter~\ref{CamlHaskellExtraction}), on which it is based.
+Indeed, the extraction of functional terms (\Coq\ objects) is first
+performed by the module \texttt{Extraction}, and the extraction of
+imperative programs comes after.
+Therefore, we have kept the same syntax as for functional terms:
+$$
+\mbox{\tt Write Caml File "\str" [ \ident$_1$ \dots\ \ident$_n$ ].} 
+$$
+where \str\ is the name given to the file to be produced (the suffix
+{\tt .ml} is added if necessary), and \ident$_1$ \dots\ \ident$_n$ the
+names of the objects to be extracted. 
+That list may contain functional and imperative objects, and does not need
+to be exhaustive.
+
+Of course, you can use the extraction facilities described in
+chapter~\ref{CamlHaskellExtraction}, namely the \texttt{ML Import},
+\texttt{Link} and \texttt{Extract} commands.
+
+
+\paragraph{The case of integers}
+There is no use of the \ocaml\ native integers: indeed, it would not be safe
+to use the machine integers while the correctness proof is done
+with unbounded integers (\texttt{nat}, \texttt{Z} or whatever type).
+But since \ocaml\ arrays are indexed over the type \texttt{int}
+(the machine integers) arrays indexes are converted from \texttt{Z}
+to \texttt{int} when necessary (the conversion is very fast: due
+to the binary representation of integers in type \texttt{Z}, it
+will never exceed thirty elementary steps).
+
+And it is also safe, since the size of a \ocaml\ array can not be greater
+than the maximum integer ($2^{30}-1$) and since the correctness proof
+establishes that indexes are always within the bounds of arrays
+(Therefore, indexes will never be greater than the maximum integer,
+and the conversion will never produce an overflow).
+
+
+%%%%%%%%%%%%
+% Examples %
+%%%%%%%%%%%%
+
+\asection{Examples}\label{prog:examples}
+
+\asubsection{Computation of $X^n$}
+
+As a first example, we prove the correctness of a program computing
+$X^n$ using the following equations:
+$$
+\left\{
+\begin{array}{lcl}
+X^{2n}   & = & (X^n)^2 \\
+X^{2n+1} & = & X \times (X^n)^2
+\end{array}
+\right.
+$$
+If $x$ and $n$ are variables containing the input and $y$ a variable that will
+contain the result ($x^n$), such a program may be the following one:
+\begin{center}
+  \begin{minipage}{8cm}
+  \begin{tabbing}
+    AA\=\kill
+    $m$ := $!x$ ; $y$ := $1$ ; \\
+    \kw{while} $!n \not= 0$ \kw{do} \\
+    \> \kw{if} $(odd ~ !n)$ \kw{then} $y$ := $!y \times !m$ ;\\
+    \> $m$ := $!m \times !m$ ; \\
+    \> $n$ := $!n / 2$ \\
+    \kw{done} \\
+  \end{tabbing}
+  \end{minipage}
+\end{center}
+
+
+\paragraph{Specification part.}
+
+Here we choose to use the binary integers of \texttt{ZArith}.
+The exponentiation $X^n$ is defined, for $n \ge 0$, in the module 
+\texttt{Zpower}:
+\begin{coq_example*}
+Require ZArith.
+Require Zpower.
+\end{coq_example*}
+
+In particular, the module \texttt{ZArith} loads a module \texttt{Zmisc}
+which contains the definitions of the predicate \texttt{Zeven} and
+\texttt{Zodd}, and the function \texttt{Zdiv2}.
+This module \texttt{ProgBool} also contains a test function
+\texttt{Zeven\_odd\_bool} of type 
+$\forall n. \exists b. \myifthenelse{b}{(Zeven~n)}{(Zodd~n)}$
+derived from the proof \texttt{Zeven\_odd\_dec},
+as explained in section~\ref{prog:booleans}:
+
+\begin{coq_eval}
+Require Ring.
+\end{coq_eval}
+
+
+\paragraph{Correctness part.}
+
+Then we come to the correctness proof. We first import the \Coq\
+module \texttt{Correctness}:
+\begin{coq_example*}
+Require Correctness.
+\end{coq_example*}
+\begin{coq_eval}
+Definition Zsquare := [n:Z](Zmult n n).
+Definition Zdouble := [n:Z]`2*n`.
+\end{coq_eval}
+
+Then we introduce all the variables needed by the program:
+\begin{coq_example*}
+Parameter x : Z.
+Global Variable n,m,y : Z ref.
+\end{coq_example*}
+
+At last, we can give the annotated program:
+\begin{coq_example}
+Correctness i_exp
+  { `n >= 0` }
+  begin
+     m := x; y := 1;
+     while !n > 0 do
+       { invariant (Zpower x n@0)=(Zmult y (Zpower m n)) /\ `n >= 0`
+         variant n }
+       (if not (Zeven_odd_bool !n) then y := (Zmult !y !m))
+          { (Zpower x n@0) = (Zmult y (Zpower m (Zdouble (Zdiv2 n)))) };
+       m := (Zsquare !m);
+       n := (Zdiv2 !n)
+     done
+   end
+   { y=(Zpower x n@0) }
+.
+\end{coq_example}
+
+The proof obligations require some lemmas involving \texttt{Zpower} and
+\texttt{Zdiv2}. You can find the whole proof in the  \Coq\ standard
+library (see below).
+Let us make some quick remarks about this program and the way it was
+written: 
+\begin{itemize}
+  \item The name \verb!n@0! is used to refer to the initial value of
+    the variable \verb!n!, as well inside the loop invariant as in
+    the post-condition;
+
+  \item Purely functional expressions are allowed anywhere in the
+    program and they can use any purely informative \Coq\ constants;
+    That is why we can use \texttt{Zmult}, \texttt{Zsquare} and
+    \texttt{Zdiv2} in the programs even if they are not other functions
+    previously introduced as programs.
+\end{itemize}
+
+
+\asubsection{A recursive program}
+
+To give an example of a recursive program, let us rewrite the previous
+program into a recursive one. We obtain the following program:
+\begin{center}
+  \begin{minipage}{8cm}
+  \begin{tabbing}
+    AA\=AA\=AA\=\kill
+    \kw{let} \kw{rec} $exp$ $x$ $n$ = \\
+    \> \kw{if} $n = 0$ \kw{then} \\
+    \> \> 1 \\
+    \> \kw{else} \\
+    \> \> \kw{let} $y$ = $(exp ~ x ~ (n/2))$ \kw{in} \\
+    \> \> \kw{if} $(even ~ n)$ \kw{then} $y\times y$ 
+                               \kw{else} $x\times (y\times y)$ \\
+  \end{tabbing}
+  \end{minipage}
+\end{center}
+
+This recursive program, once it is annotated, is given to the
+tactic \texttt{Correctness}:
+\begin{coq_eval}
+Reset n.
+\end{coq_eval}
+\begin{coq_example}
+Correctness r_exp
+  let rec exp (x:Z) (n:Z) : Z { variant n } =
+    { `n >= 0` }
+    (if n = 0 then
+       1
+     else
+       let y = (exp x (Zdiv2 n)) in
+       (if (Zeven_odd_bool n) then
+          (Zmult y y)
+        else
+          (Zmult x (Zmult y y))) { result=(Zpower x n) }
+    ) 
+    { result=(Zpower x n) }
+.
+\end{coq_example}
+
+You can notice that the specification is simpler in the recursive case:
+we only have to give the pre- and post-conditions --- which are the same
+as for the imperative version --- but there is no annotation
+corresponding to the loop invariant.
+The other two annotations in the recursive program are added for the
+recursive call and for the test inside the \textsf{let in} construct
+(it can not be done automatically in general,
+so the user has to add it by himself).
+
+
+\asubsection{Other examples}
+
+You will find some other examples with the distribution of the system
+\Coq, in the sub-directory \verb!contrib/correctness! of the
+\Coq\ standard library. Those examples are mostly programs to compute
+the factorial and the exponentiation in various ways (on types \texttt{nat}
+or \texttt{Z}, in imperative way or recursively, with global
+variables or as functions, \dots).
+
+There are also some bigger correctness developments in the 
+\Coq\ contributions, which are available on the web page
+\verb!coq.inria.fr/contribs!.
+for the moment, you can find:
+\begin{itemize}
+  \item A proof of \emph{insertion sort} by Nicolas Magaud, ENS Lyon;
+  \item Proofs of \emph{quicksort}, \emph{heapsort} and \emph{find} by
+    the author.
+\end{itemize}
+These examples are fully detailed in~\cite{FilliatreMagaud99,Filliatre99c}.
+
+
+%%%%%%%%%%%%%%%
+% BUG REPORTS %
+%%%%%%%%%%%%%%%
+
+\asection{Bugs}
+
+\begin{itemize}
+  \item There is no discharge mechanism for programs; so you
+    \emph{cannot} do a program's proof inside a section (actually,
+    you can do it, but your program will not exist anymore after having
+    closed the section).
+\end{itemize}
+
+Surely there are still many bugs in this implementation.
+Please send bug reports to \textsf{Jean-Christophe.Filliatre$@$lri.fr}.
+Don't forget to send the version of \Coq\ used (given by
+\texttt{coqtop -v}) and a script producing the bug.
+
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "Reference-Manual"
+%%% End: