From 80b2152f54956ca171eb61e8a25d99c93cbc174c Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 11 Apr 2001 13:02:06 +0000
Subject: documentation automatique de la biblio standard

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8188 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/Programs.tex | 929 -------------------------------------------------------
 1 file changed, 929 deletions(-)
 delete mode 100644 doc/Programs.tex

(limited to 'doc/Programs.tex')

diff --git a/doc/Programs.tex b/doc/Programs.tex
deleted file mode 100644
index 4ff14eb636..0000000000
--- a/doc/Programs.tex
+++ /dev/null
@@ -1,929 +0,0 @@
-\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.}}
-$$
-\emph{Be aware that this tactic is still very experimental}.
-
-
-%%%%%%%%%%%%%%%%%%%%%
-% 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: 
-- 
cgit v1.2.3

