From 6e69f156d5c27348370a739b74bb9be943b32ff8 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Fri, 13 Jan 2017 02:19:35 -0500
Subject: [PATCH] books/bookvol13 pre/post conditions and Coq nat vs Axiom NNI
Goal: Proving Axiom Correct
\index{Boldo, Sylvie}
\index{March\'e, Claude}
\begin{chunk}{axiom.bib}
@article{Bold11,
author = "Boldo, Sylvie and Marche, Claude",
title = "Formal verification of numerical programs: from C annotated
programs to mechanical proofs",
year = "2011",
publisher = "Springer",
journal = "Mathematics in Computer Science",
volume = "5",
pages = "377-393",
link = "\url{https://hal.archives-ouvertes.fr/hal-00777605/document}",
abstract =
"Numerical programs may require a high level of guarantee. This can be
achieved by applying formal methods, such as machine-checked proofs.
But these tools handle mathematical theorems while we are interested
in C code, in which numerical computations are performed using
floating-point arithmetic, whereas proof tools typically handle exact
real arithmetic. To achieve this high level of confidence on C programs,
we use a chain of tools: Frama-C, its Jessie plugin, Why and provers
among Coq, Gappa, Alt-Ergo, CVC3 and Z3. This approach requires the C
program to be annotated; each function must be precisely specified, and
we prove the correctness of the program by proving both that it meets its
specifications and that no runtime error may occur. The purpose of this
paper is to illustrate, on various examples, the features of this
approach.",
paper = "Bold11.pdf"
}
\end{chunk}
\index{Boldo, Sylvie}
\index{Filliatre, Jean-Christophe}
\begin{chunk}{axiom.bib}
@misc{Bold07,
author = "Boldo, Sylvie and Filliatre, Jean-Christophe}",
title = "Formal Verification of Floating-Point programs",
link = "\url{http://www-lipn.univ-paris13.fr/CerPAN/files/ARITH.pdf}",
paper = "Bold07.pdf"
}
\end{chunk}
\index{Boldo, Sylvie}
\index{Filliatre, Jean-Christophe}
\begin{chunk}{axiom.bib}
@misc{Bold07a,
author = "Boldo, Sylvie and Filliatre, Jean-Christophe",
title = "Formal Verification of Floating-Point programs",
link = "\url{http://www.lri.fr/~filliatr/ftp/publis/caduceus-floats.pdf}",
abstract =
"This paper introduces a methodology to perform formal verification of
floating-point C programs. It extends an existing tool for
verification of C programs, Caduceus, with new annotations for
specific floating-point arithmetic. The Caduceus first-order logic
model for C programs is extended accordingly. Then verification
conditions are obtained in the usual way and can be discharged
interactively with the Coqa proof assistant, using an existing Coq
formalization of floating-point arithmetic. This methodology is
already implemented and has been successfully applied to several short
floating-point programs, which are presented in this paper.",
paper = "Bold07a.pdf"
}
\end{chunk}
\index{Wadler, Philip}
\begin{chunk}{axiom.bib}
@misc{Wadl14,
author = "Wadler, Philip",
title = "Propositions as Types",
year = "2014",
link = "\url{http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf}",
paper = "Wadl14.pdf"
}
\end{chunk}
\begin{chunk}{axiom.bib}
@misc{COQnat,
author = "COQ Proof Assistant",
title = "{Library} {Coq}.{Init}.{Nat}",
link = "\url{https://coq.inria.fr/library/Coq.Init.Nat.html}",
abstract = "Peano natural numbers, defintions of operations",
year = "2017"
}
\end{chunk}
---
books/bookvol13.pamphlet | 367 ++++++++++++++++++++++++++++++++++++++++
books/bookvolbib.pamphlet | 90 ++++++++++
changelog | 3 +
patch | 90 +++++++++-
src/axiom-website/patches.html | 4 +-
5 files changed, 547 insertions(+), 7 deletions(-)
diff --git a/books/bookvol13.pamphlet b/books/bookvol13.pamphlet
index 612ecdd..329afd5 100644
--- a/books/bookvol13.pamphlet
+++ b/books/bookvol13.pamphlet
@@ -1686,6 +1686,58 @@ end nat
\end{verbatim}
+\chapter{Formal Pre- and Post-conditions}
+In Boldo\cite{Bold11} we find an effort to verify floating point software
+using preconditions, postconditions, and assertions. Quoting:
+
+``These conjectures can be described formally by annotations as follows.
+\begin{verbatim}
+/*@ requires \abs(x) <= 0x1p-5;
+ @ ensures \abs(\result - \cos(x)) <= 0x1p-23;
+ @*/
+float my_cosine(float x) {
+ //@ assert \abs(1.0 - x*x*0.5 - \cos(x)) < 0x1p-24;
+ return 1.0f - x * x * 0.5f;
+}
+\end{verbatim}
+The {\sl precondition}, introduced by {\bf requires}, states that we expect
+argument {\sl x} in the interval [-1/32; 1/32]. The {\sl postcondition},
+introduced by {\bf ensures}, states that the distance between the value
+returned by the function, denoted by the keyword {\bf \verb|\result|}, and the
+model of the program, which is here the true mathematical cosine function
+denoted by {\bf \verb|\cos|} in ACSL, is not greater than $2^{-23}$. It is
+important to notice that in annotations the operators like $+$ or $*$
+denote operations on real numbers and not on floating-point numbers. In
+particular, there is no rounding error and no overflow in annotations,
+unlike in the early Leavens' proposal. The C variables of type {\tt float},
+like {\tt x} and {\tt \verb|\result|} in this example, are interpreted as the
+real number they represent. Thus, the last annotation, given as an
+assertion inside the code, is a way to make explicit the reasoning we made
+above, making the total error the sum of the method error and the rounding
+error: it states that the method error is less than $2^{-24}$. Again, it
+is thanks to the choice of having exact operations in the annotations that
+we are able to state a property of the method error.''
+
+In Boldo\cite{Bold07,Bold07a} we find 'search in an array' annotated:
+\begin{verbatim}
+/*@ requires \valid_range(t,0,n-1)
+ @ ensures
+ @ (0 <= \result < n => t[\result] == v) &&
+ @ (\result == n =>
+ @ \forall int i; 0 <= i < n => t[i] != v) */
+int index(int t[], int n, int v) {
+ int i = 0;
+ /*@ invariant 0 <= i &&
+ @ \forall int k; 0 <= k * t[k] != v
+ @ variant n - i */
+ while (i < n) {
+ if (t[i] == v) break;
+ i++;
+ }
+ return i;
+}
+\end{verbatim}
+
\chapter{Types and Signatures}
We need to start from a base of the existing types in Common Lisp,
@@ -1701,6 +1753,321 @@ Axiom adds these types:
\item Command = String
\end{itemize}
+\chapter{COQ nat vs Axiom NNI}
+
+COQ's nat domain includes a proof of GCD.
+
+We would like to show an isomorphism between types in Coq and
+types in Axiom. Having such an isomorphism will make lemmas
+available and simplify future proofs.
+
+Note that Coq's {\tt nat} domain stops at O (a symbolic 0)
+as does Axiom's NNI. The Axiom interpreter will promote a
+subtraction to Integer whereas Coq will not.
+
+COQ's nat domain\cite{COQnat} is
+
+\subsection{Library Coq.Init.Nat}
+
+\begin{verbatim}
+Require Import Notations Logic Datatypes.
+
+Local Open Scope nat_scope.
+\end{verbatim}
+
+{\bf Peano natural numbers, definitions of operations}
+
+This file is meant to be used as a whole module, without importing it,
+leading to qualified definitions (e.g. Nat.pred)
+
+\begin{verbatim}
+Definition t := nat.
+\end{verbatim}
+
+{\bf Constants}
+
+\begin{verbatim}
+Definition zero := 0.
+Definition one := 1.
+Definition two := 2.
+\end{verbatim}
+
+{\bf Basic operations}
+
+\begin{verbatim}
+Definition succ := S.
+
+Definition pred n :=
+ match n with
+ | 0 => n
+ | S u => u
+ end.
+
+Fixpoint add n m :=
+ match n with
+ | 0 => m
+ | S p => S (p + m)
+ end
+
+where "n + m" := (add n m) : nat_scope.
+
+Definition double n := n + n.
+
+Fixpoint mul n m :=
+ match n with
+ | 0 => 0
+ | S p => m + p * m
+ end
+
+where "n * m" := (mul n m) : nat_scope.
+
+\end{verbatim}
+
+Note that Axiom's NNI domain will be automatically promoted to Integer
+when the subtraction result is negative. Coq returns O when this occurs.
+
+\begin{verbatim}
+Truncated subtraction: n-m is 0 if n<=m
+
+Fixpoint sub n m :=
+ match n, m with
+ | S k, S l => k - l
+ | _, _ => n
+ end
+
+where "n - m" := (sub n m) : nat_scope.
+
+\end{verbatim}
+{\bf Comparisons}
+\begin{verbatim}
+
+Fixpoint eqb n m : bool :=
+ match n, m with
+ | 0, 0 => true
+ | 0, S _ => false
+ | S _, 0 => false
+ | S n', S m' => eqb n' m'
+ end.
+
+Fixpoint leb n m : bool :=
+ match n, m with
+ | 0, _ => true
+ | _, 0 => false
+ | S n', S m' => leb n' m'
+ end.
+
+Definition ltb n m := leb (S n) m.
+
+Infix "=?" := eqb (at level 70) : nat_scope.
+Infix "<=?" := leb (at level 70) : nat_scope.
+Infix " Eq
+ | 0, S _ => Lt
+ | S _, 0 => Gt
+ | S n', S m' => compare n' m'
+ end.
+
+Infix "?=" := compare (at level 70) : nat_scope.
+
+\end{verbatim}
+{\bf Minimum, maximum}
+\begin{verbatim}
+
+Fixpoint max n m :=
+ match n, m with
+ | 0, _ => m
+ | S n', 0 => n
+ | S n', S m' => S (max n' m')
+ end.
+
+Fixpoint min n m :=
+ match n, m with
+ | 0, _ => 0
+ | S n', 0 => 0
+ | S n', S m' => S (min n' m')
+ end.
+
+\end{verbatim}
+{\bf Parity tests}
+\begin{verbatim}
+
+Fixpoint even n : bool :=
+ match n with
+ | 0 => true
+ | 1 => false
+ | S (S n') => even n'
+ end.
+
+Definition odd n := negb (even n).
+
+\end{verbatim}
+{\bf Power}
+\begin{verbatim}
+
+Fixpoint pow n m :=
+ match m with
+ | 0 => 1
+ | S m => n * (n^m)
+ end
+
+where "n ^ m" := (pow n m) : nat_scope.
+
+\end{verbatim}
+{\bf Euclidean division}
+\begin{verbatim}
+This division is linear and tail-recursive. In divmod, y is the
+predecessor of the actual divisor, and u is y minus the real remainder
+
+Fixpoint divmod x y q u :=
+ match x with
+ | 0 => (q,u)
+ | S x' => match u with
+ | 0 => divmod x' y (S q) y
+ | S u' => divmod x' y q u'
+ end
+ end.
+
+Definition div x y :=
+ match y with
+ | 0 => y
+ | S y' => fst (divmod x y' 0 y')
+ end.
+
+Definition modulo x y :=
+ match y with
+ | 0 => y
+ | S y' => y' - snd (divmod x y' 0 y')
+ end.
+
+Infix "/" := div : nat_scope.
+Infix "mod" := modulo (at level 40, no associativity) : nat_scope.
+
+\end{verbatim}
+{\bf Greatest common divisor}
+\begin{verbatim}
+We use Euclid algorithm, which is normally not structural, but Coq is
+now clever enough to accept this (behind modulo there is a subtraction,
+which now preserves being a subterm)
+
+Fixpoint gcd a b :=
+ match a with
+ | O => b
+ | S a' => gcd (b mod (S a')) (S a')
+ end.
+
+\end{verbatim}
+{\bf Square}
+\begin{verbatim}
+
+Definition square n := n * n.
+
+\end{verbatim}
+{\bf Square root}
+\begin{verbatim}
+
+The following square root function is linear (and tail-recursive).
+With Peano representation, we can't do better. For faster algorithm,
+see Psqrt/Zsqrt/Nsqrt... We search the square root of
+n = k + p^2 + (q - r) with q = 2p and 0<=r<=q. We start with
+p=q=r=0, hence looking for the square root of n = k. Then we
+progressively decrease k and r. When k = S k' and r=0, it means we can
+use (S p) as new sqrt candidate, since (S k')+p^2+2p = k'+(S
+p)^2. When k reaches 0, we have found the biggest p^2 square contained
+in n, hence the square root of n is p.
+
+Fixpoint sqrt_iter k p q r :=
+ match k with
+ | O => p
+ | S k' => match r with
+ | O => sqrt_iter k' (S p) (S (S q)) (S (S q))
+ | S r' => sqrt_iter k' p q r'
+ end
+ end.
+
+Definition sqrt n := sqrt_iter n 0 0 0.
+
+\end{verbatim}
+{\bf Log2}
+\begin{verbatim}
+This base-2 logarithm is linear and tail-recursive. In
+log2_iter, we maintain the logarithm p of the counter q, while r is
+the distance between q and the next power of 2, more precisely q + S r
+= 2^(S p) and r<2^p. At each recursive call, q goes up while r goes
+down. When r is 0, we know that q has almost reached a power of 2, and
+we increase p at the next call, while resetting r to q. Graphically
+(numbers are q, stars are r) :
+
+ 10
+ 9
+ 8
+ 7 *
+ 6 *
+ 5 ...
+ 4
+ 3 *
+ 2 *
+ 1 * *
+0 * * *
+
+We stop when k, the global downward counter reaches 0. At that moment,
+q is the number we're considering (since k+q is invariant), and p its
+logarithm.
+
+Fixpoint log2_iter k p q r :=
+ match k with
+ | O => p
+ | S k' => match r with
+ | O => log2_iter k' (S p) (S q) q
+ | S r' => log2_iter k' p (S q) r'
+ end
+ end.
+
+Definition log2 n := log2_iter (pred n) 0 1 0.
+
+Iterator on natural numbers
+
+Definition iter (n:nat) {A} (f:A->A) (x:A) : A :=
+ nat_rect (fun _ => A) x (fun _ => f) n.
+
+Bitwise operations We provide here some bitwise operations for unary
+numbers. Some might be really naive, they are just there for
+fullfiling the same interface as other for natural representations. As
+soon as binary representations such as NArith are available, it is
+clearly better to convert to/from them and use their ops.
+
+Fixpoint div2 n :=
+ match n with
+ | 0 => 0
+ | S 0 => 0
+ | S (S n') => S (div2 n')
+ end.
+
+Fixpoint testbit a n : bool :=
+ match n with
+ | 0 => odd a
+ | S n => testbit (div2 a) n
+ end.
+
+Definition shiftl a := nat_rect _ a (fun _ => double).
+Definition shiftr a := nat_rect _ a (fun _ => div2).
+
+Fixpoint bitwise (op:bool->bool->bool) n a b :=
+ match n with
+ | 0 => 0
+ | S n' =>
+ (if op (odd a) (odd b) then 1 else 0) +
+ 2*(bitwise op n' (div2 a) (div2 b))
+ end.
+
+Definition land a b := bitwise andb a a b.
+Definition lor a b := bitwise orb (max a b) a b.
+Definition ldiff a b := bitwise (fun b b' => andb b (negb b')) a a b.
+Definition lxor a b := bitwise xorb (max a b) a b.
+\end{verbatim}
+
\chapter{Other Ideas to Explore}
Computerising Mathematical Text\cite{Kama15} explores various ways of
capturing mathematical reasoning.
diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 44c992e..b692b79 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -5352,6 +5352,17 @@ Mathematics of Computation, Vol 32, No 144 Oct 1978, pp1215-1231
\section{Proving Axiom Correct} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{chunk}{axiom.bib}
+@misc{COQnat,
+ author = "COQ Proof Assistant",
+ title = "{Library} {Coq}.{Init}.{Nat}",
+ link = "\url{https://coq.inria.fr/library/Coq.Init.Nat.html}",
+ abstract = "Peano natural numbers, defintions of operations",
+ year = "2017"
+}
+
+\end{chunk}
+
+\begin{chunk}{axiom.bib}
@book{Acze13,
author = "Aczel, Peter et al.",
title = "Homotopy Type Theory: Univalent Foundations of Mathematics",
@@ -5587,6 +5598,73 @@ Martin, U.
\end{chunk}
\index{Boldo, Sylvie}
+\index{Filliatre, Jean-Christophe}
+\begin{chunk}{axiom.bib}
+@misc{Bold07,
+ author = "Boldo, Sylvie and Filliatre, Jean-Christophe",
+ title = "Formal Verification of Floating-Point programs",
+ link = "\url{http://www-lipn.univ-paris13.fr/CerPAN/files/ARITH.pdf}",
+ paper = "Bold07.pdf"
+}
+
+\end{chunk}
+
+\index{Boldo, Sylvie}
+\index{Filliatre, Jean-Christophe}
+\begin{chunk}{axiom.bib}
+@misc{Bold07a,
+ author = "Boldo, Sylvie and Filliatre, Jean-Christophe",
+ title = "Formal Verification of Floating-Point programs",
+ link = "\url{http://www.lri.fr/~filliatr/ftp/publis/caduceus-floats.pdf}",
+ abstract =
+ "This paper introduces a methodology to perform formal verification of
+ floating-point C programs. It extends an existing tool for
+ verification of C programs, Caduceus, with new annotations for
+ specific floating-point arithmetic. The Caduceus first-order logic
+ model for C programs is extended accordingly. Then verification
+ conditions are obtained in the usual way and can be discharged
+ interactively with the Coqa proof assistant, using an existing Coq
+ formalization of floating-point arithmetic. This methodology is
+ already implemented and has been successfully applied to several short
+ floating-point programs, which are presented in this paper.",
+ paper = "Bold07a.pdf"
+}
+
+\end{chunk}
+
+\index{Boldo, Sylvie}
+\index{March\'e, Claude}
+\begin{chunk}{axiom.bib}
+@article{Bold11,
+ author = "Boldo, Sylvie and Marche, Claude",
+ title = "Formal verification of numerical programs: from C annotated
+ programs to mechanical proofs",
+ year = "2011",
+ publisher = "Springer",
+ journal = "Mathematics in Computer Science",
+ volume = "5",
+ pages = "377-393",
+ link = "\url{https://hal.archives-ouvertes.fr/hal-00777605/document}",
+ abstract =
+ "Numerical programs may require a high level of guarantee. This can be
+ achieved by applying formal methods, such as machine-checked proofs.
+ But these tools handle mathematical theorems while we are interested
+ in C code, in which numerical computations are performed using
+ floating-point arithmetic, whereas proof tools typically handle exact
+ real arithmetic. To achieve this high level of confidence on C programs,
+ we use a chain of tools: Frama-C, its Jessie plugin, Why and provers
+ among Coq, Gappa, Alt-Ergo, CVC3 and Z3. This approach requires the C
+ program to be annotated; each function must be precisely specified, and
+ we prove the correctness of the program by proving both that it meets its
+ specifications and that no runtime error may occur. The purpose of this
+ paper is to illustrate, on various examples, the features of this
+ approach.",
+ paper = "Bold11.pdf"
+}
+
+\end{chunk}
+
+\index{Boldo, Sylvie}
\begin{chunk}{axiom.bib}
@misc{Bold16,
author = "Boldo, Sylvie",
@@ -7488,6 +7566,18 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
\end{chunk}
+\index{Wadler, Philip}
+\begin{chunk}{axiom.bib}
+@misc{Wadl14,
+ author = "Wadler, Philip",
+ title = "Propositions as Types",
+ year = "2014",
+ link = "\url{http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf}",
+ paper = "Wadl14.pdf"
+}
+
+\end{chunk}
+
\begin{chunk}{axiom.bib}
@misc{Wiki17,
author = "Wikipedia",
diff --git a/changelog b/changelog
index 49b0883..7a27853 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,6 @@
+20170113 tpd src/axiom-website/patches.html 20170113.01.tpd.patch
+20170113 tpd books/bookvol13 pre/post conditions and Coq nat vs Axiom NNI
+20170113 tpd books/bookvolbib pre/post conditions and Coq nat vs Axiom NNI
20170112 tpd src/axiom-website/patches.html 20170112.03.tpd.patch
20170112 tpd books/bookvolbib Formal verif. of numerical analysis programs
20170112 tpd src/axiom-website/patches.html 20170112.02.tpd.patch
diff --git a/patch b/patch
index 4e8efba..693790e 100644
--- a/patch
+++ b/patch
@@ -1,16 +1,94 @@
-books/bookvolbib Formal verification of numerical analysis programs
+books/bookvol13 pre/post conditions and Coq nat vs Axiom NNI
Goal: Proving Axiom Correct
\index{Boldo, Sylvie}
+\index{March\'e, Claude}
\begin{chunk}{axiom.bib}
-@misc{Bold16,
- author = "Boldo, Sylvie",
- title = "Formal verification of numerical analysis programs",
- year = "2016",
- link = "\url{https://www.youtube.com/watch?v=7MDwpwD6Ts4}"
+@article{Bold11,
+ author = "Boldo, Sylvie and Marche, Claude",
+ title = "Formal verification of numerical programs: from C annotated
+ programs to mechanical proofs",
+ year = "2011",
+ publisher = "Springer",
+ journal = "Mathematics in Computer Science",
+ volume = "5",
+ pages = "377-393",
+ link = "\url{https://hal.archives-ouvertes.fr/hal-00777605/document}",
+ abstract =
+ "Numerical programs may require a high level of guarantee. This can be
+ achieved by applying formal methods, such as machine-checked proofs.
+ But these tools handle mathematical theorems while we are interested
+ in C code, in which numerical computations are performed using
+ floating-point arithmetic, whereas proof tools typically handle exact
+ real arithmetic. To achieve this high level of confidence on C programs,
+ we use a chain of tools: Frama-C, its Jessie plugin, Why and provers
+ among Coq, Gappa, Alt-Ergo, CVC3 and Z3. This approach requires the C
+ program to be annotated; each function must be precisely specified, and
+ we prove the correctness of the program by proving both that it meets its
+ specifications and that no runtime error may occur. The purpose of this
+ paper is to illustrate, on various examples, the features of this
+ approach.",
+ paper = "Bold11.pdf"
+}
+
+\end{chunk}
+
+\index{Boldo, Sylvie}
+\index{Filliatre, Jean-Christophe}
+\begin{chunk}{axiom.bib}
+@misc{Bold07,
+ author = "Boldo, Sylvie and Filliatre, Jean-Christophe}",
+ title = "Formal Verification of Floating-Point programs",
+ link = "\url{http://www-lipn.univ-paris13.fr/CerPAN/files/ARITH.pdf}",
+ paper = "Bold07.pdf"
+}
+
+\end{chunk}
+
+\index{Boldo, Sylvie}
+\index{Filliatre, Jean-Christophe}
+\begin{chunk}{axiom.bib}
+@misc{Bold07a,
+ author = "Boldo, Sylvie and Filliatre, Jean-Christophe",
+ title = "Formal Verification of Floating-Point programs",
+ link = "\url{http://www.lri.fr/~filliatr/ftp/publis/caduceus-floats.pdf}",
+ abstract =
+ "This paper introduces a methodology to perform formal verification of
+ floating-point C programs. It extends an existing tool for
+ verification of C programs, Caduceus, with new annotations for
+ specific floating-point arithmetic. The Caduceus first-order logic
+ model for C programs is extended accordingly. Then verification
+ conditions are obtained in the usual way and can be discharged
+ interactively with the Coqa proof assistant, using an existing Coq
+ formalization of floating-point arithmetic. This methodology is
+ already implemented and has been successfully applied to several short
+ floating-point programs, which are presented in this paper.",
+ paper = "Bold07a.pdf"
+}
+
+\end{chunk}
+
+\index{Wadler, Philip}
+\begin{chunk}{axiom.bib}
+@misc{Wadl14,
+ author = "Wadler, Philip",
+ title = "Propositions as Types",
+ year = "2014",
+ link = "\url{http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf}",
+ paper = "Wadl14.pdf"
}
\end{chunk}
+\begin{chunk}{axiom.bib}
+@misc{COQnat,
+ author = "COQ Proof Assistant",
+ title = "{Library} {Coq}.{Init}.{Nat}",
+ link = "\url{https://coq.inria.fr/library/Coq.Init.Nat.html}",
+ abstract = "Peano natural numbers, defintions of operations",
+ year = "2017"
+}
+
+\end{chunk}
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index 30aad89..e94fe55 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -5631,7 +5631,9 @@ books/bookvolbib References on Program Proofs*

20170112.02.tpd.patch
books/bookvolbib Using Latex as a Semantic Markup Format

20170112.03.tpd.patch
-Formal verification of numerical analysis programs

+books/bookvolbib Formal verification of numerical analysis programs

+20170113.01.tpd.patch
+books/bookvol13 pre/post conditions and Coq nat vs Axiom NNI

--
1.7.5.4