From b50a9184b9927c36ec53cd4b88d0e2f45f94b4c6 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 9 Apr 2001 07:33:29 +0000
Subject: mise ļæ½ jour V7; biblio Correctness

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8174 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/Extraction.tex   |  4 ++--
 doc/Programs.tex     | 28 +++++++++++++---------------
 doc/RefMan-tacex.tex |  6 ++++--
 doc/biblio.bib       | 39 +++++++++++++++++++++++++++++++++++++++
 4 files changed, 58 insertions(+), 19 deletions(-)

diff --git a/doc/Extraction.tex b/doc/Extraction.tex
index a9f23768b3..230fa056f4 100755
--- a/doc/Extraction.tex
+++ b/doc/Extraction.tex
@@ -3,10 +3,10 @@
 \aauthor{Jean-Christophe Filliātre and Pierre Letouzey}
 \index{Extraction}
 
-\begin{center}
+\begin{flushleft}
   \em The status of extraction is experimental \\
   Haskell extraction is not yet implemented
-\end{center}
+\end{flushleft}
 
 It is possible to use \Coq\ to build certified and relatively
 efficient programs, extracting them from the proofs of their
diff --git a/doc/Programs.tex b/doc/Programs.tex
index e92dd59311..4ff14eb636 100644
--- a/doc/Programs.tex
+++ b/doc/Programs.tex
@@ -11,17 +11,13 @@
 This chapter describes a new tactic
 to prove the correctness and termination of imperative
 programs annotated in a Floyd-Hoare logic style.
-This tactic is provided in the \Coq\ module \texttt{Programs},
+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 Programs.}}
-$$
-If you want to use this tactic with the native-code version of \Coq,
-you will have to run the version of \Coq\ with all the tactics, through
-the command
-$$
-\mbox{\texttt{coqtop -full}}
+\mbox{\texttt{Require Correctness.}}
 $$
 \emph{Be aware that this tactic is still very experimental}.
 
@@ -70,7 +66,7 @@ vernacular command (which creates the goal from the annotated program)
 and a tactic (which partially solves it, leaving some proof
 obligations to the user).
 
-Whereas \texttt{Correctness} is not a tactic, the following syntax is
+Although \texttt{Correctness} is not a tactic, the following syntax is
 available:  
 $$
 \mbox{\tt Correctness} ~~ ident ~~ annotated\_program ~ ; ~ tactic.
@@ -484,7 +480,7 @@ $\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 Programs standard library comes
+In particular, the \texttt{Correctness} standard library comes
 with a bunch of decidability theorems on type \texttt{nat}:
 $$
 \begin{array}{ll}
@@ -624,7 +620,7 @@ Regarding the post-condition of $f$, there are different possible cases:
 The tactic comes with some libraries, useful to write programs and
 specifications.
 The first set of libraries is automatically loaded with the module
-\texttt{Programs}. Among them, you can find the modules:
+\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
@@ -784,9 +780,9 @@ Require Ring.
 \paragraph{Correctness part.}
 
 Then we come to the correctness proof. We first import the \Coq\
-module \texttt{Programs}:
+module \texttt{Correctness}:
 \begin{coq_example*}
-Require Programs.
+Require Correctness.
 \end{coq_example*}
 \begin{coq_eval}
 Definition Zsquare := [n:Z](Zmult n n).
@@ -890,7 +886,7 @@ 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!tactics/programs/EXAMPLES! of the
+\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
@@ -902,8 +898,10 @@ There are also some bigger correctness developments in the
 for the moment, you can find:
 \begin{itemize}
   \item A proof of \emph{insertion sort} by Nicolas Magaud, ENS Lyon;
-  \item A proof of \emph{quicksort} and \emph{find} by the author.
+  \item Proofs of \emph{quicksort}, \emph{heapsort} and \emph{find} by
+    the author.
 \end{itemize}
+These examples are fully detailed in~\cite{FilliatreMagaud99,Filliatre99c}.
 
 
 %%%%%%%%%%%%%%%
diff --git a/doc/RefMan-tacex.tex b/doc/RefMan-tacex.tex
index acb57e41a9..49dd8a437e 100644
--- a/doc/RefMan-tacex.tex
+++ b/doc/RefMan-tacex.tex
@@ -638,10 +638,12 @@ Undo. Quote interp_f [B C iff].
 \end{coq_example}
 
 \Warning  This tactic is new and experimental. Since function inversion
-is undecidable in general case, don't expect miracles from it !
+is undecidable in general case, don't expect miracles from it!
+
+% \SeeAlso file \texttt{theories/DEMOS/DemoQuote.v}
 
-\SeeAlso file \texttt{theories/DEMOS/DemoQuote.v}
 \SeeAlso comments of source file \texttt{tactics/contrib/polynom/quote.ml}
+
 \SeeAlso the tactic \texttt{Ring} (chapter \ref{Ring})
 
 
diff --git a/doc/biblio.bib b/doc/biblio.bib
index 653944c9d3..b149f557c8 100755
--- a/doc/biblio.bib
+++ b/doc/biblio.bib
@@ -393,6 +393,45 @@ s},
         YEAR               = {1995}
 }
 
+@Unpublished{Filliatre00a,
+  author = 	 {J.-C. Filli\^atre},
+  title = 	 {{Verification of Non-Functional Programs 
+                   using Interpretations in Type Theory}},
+  month =	 {February},
+  year =	 2000,
+  note = 	 {To appear in the Journal of Functional Programming.  
+                  [English translation of \cite{Filliatre99}]},
+  note =         {\url{http://www.lri.fr/~filliatr/ftp/publis/jphd.ps.gz}}
+}
+
+@PhdThesis{Filliatre99,
+  author = 	 {J.-C. Filli\^atre},
+  title = 	 {{Preuve de programmes imp\'eratifs en th\'eorie des types}},
+  type =         {Th{\`e}se de Doctorat},
+  school = 	 {Universit\'e Paris-Sud},
+  year = 	 1999,
+  month =	 {July},
+  note =         {\url{http://www.lri.fr/~filliatr/ftp/publis/these.ps.gz}}
+}
+
+@Unpublished{Filliatre99c,
+  author = 	 {J.-C. Filli\^atre},
+  title = 	 {{Formal Proof of a Program: Find}},
+  month =        {January},
+  year =         2000,
+  note = 	 {Submitted to \emph{Science of Computer Programming}},
+  note =         {\url{http://www.lri.fr/~filliatr/ftp/publis/find.ps.gz}}
+}
+
+@InProceedings{FilliatreMagaud99,
+  author = 	 {J.-C. Filli\^atre and N. Magaud},
+  title = 	 {{Certification of sorting algorithms in the system Coq}},
+  booktitle =    {Theorem Proving in Higher Order Logics: 
+                  Emerging Trends},
+  year =	 1999,
+  note = {\url{http://www.lri.fr/~filliatr/ftp/publis/Filliatre-Magaud.ps.gz}}
+}
+
 @UNPUBLISHED{Fle90,
         AUTHOR             = {E. Fleury},
         MONTH              = jul,
-- 
cgit v1.2.3