diff options
Diffstat (limited to 'doc/Correctness.tex')
| -rw-r--r-- | doc/Correctness.tex | 930 |
1 files changed, 0 insertions, 930 deletions
diff --git a/doc/Correctness.tex b/doc/Correctness.tex deleted file mode 100644 index 2b770a877..000000000 --- a/doc/Correctness.tex +++ /dev/null @@ -1,930 +0,0 @@ -\achapter{Proof of imperative programs} -\aauthor{Jean-Christophe Filliâtre} -\label{Addoc-programs} -\index{Imperative programs!proof of} -\comindex{Correctness} - -%%%%%%%%%%%%%%%% -% Introduction % -%%%%%%%%%%%%%%%% - -\noindent\framebox{Warning:} The tactic presented in this chapter was a -prototype implementation, now deprecated and no more maintained. It is -subsumed by a much more powerful tool, developped and distributed -independently of the system \Coq, called \textsc{Why} (see -\url{http://why.lri.fr/}). - -\bigskip - -This chapter describes a 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,Filliatre03jfp}. -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'at'$. -Actually, it is possible to refer to the value of a variable at any -moment of the evaluation with the notation $x'at'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'at' < 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'at'L$. - -There is a special label $0$ which is automatically inserted at the -beginning of the program. Therefore, $x'at'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, either 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{Extraction}), 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{Extraction}, 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 Import ZArith. -Require Import 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 Import 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 Import Correctness. -Open Scope Z_scope. -\end{coq_example*} -\begin{coq_eval} -Definition Zsquare (n:Z) := 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'at'0 = y * Zpower m n /\ n >= 0) variant n } - (if (not (Zeven_odd_bool !n)) then y := (Zmult !y !m) else tt) - {Zpower x n'at'0 = y * Zpower m (Zdouble (Zdiv2 n))}; m := (Zsquare !m); - n := (Zdiv2 !n) - done - end - {y = Zpower x n'at'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'at'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: |