From 4eded4747f9e193108574cccb388f9a4e869e8e7 Mon Sep 17 00:00:00 2001 From: Tim Daly Date: Sun, 30 Aug 2015 14:36:04 -0400 Subject: [PATCH] books/bookvolbib add Tanenbaum, Knuth references Goal: Proving Axiom Correct @article{Tane76, author = "Tanenbaum, Andrew S.", title = "In Defense of Program Testing or Correctness Proofs Considered Harmf journal = "SIGPLAN Notices", volume = "11", number = "1", year = "1976", pages = "64-68", paper = "Tane76.pdf", abstract = "Dijkstra's remark to the effect that testing can only demonstrate the presence of errors and not their absence is unquestionably true. This observation, together with the recent development of techniques for formally proving programs to be correct, has led some computer scientists to believe that correctness proofs can replace testing as a means for insuring that programs do what they are supposed to do. The purpose of this note is to point out several reasons why even programs rigorously proven to be correct should be neertheless thoroughly tested. Correctness proofs can supplement, but cannot replace comprehensive testing." } @misc{Knut15, author = "Unknown", title = "Knuth & Plass line-breaking Revisited", year = "2015", url = "http://defoe.sourceforge.net/folio/knuth-plass.html" } --- books/bookvolbib.pamphlet | 33 +++++++++++++++++++++++++++++++++ changelog | 2 ++ patch | 33 ++++++++++++++++++++++++++++++--- src/axiom-website/patches.html | 2 ++ 4 files changed, 67 insertions(+), 3 deletions(-) diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet index ac43a4b..c0b3765 100644 --- a/books/bookvolbib.pamphlet +++ b/books/bookvolbib.pamphlet @@ -2718,6 +2718,29 @@ Kelsey, Tom; Martin, Ursula; Owre, Sam \end{chunk} +\index{Tanenbaum, Andrew S.} +\begin{chunk}{axiom.bib} +@article{Tane76, + author = "Tanenbaum, Andrew S.", + title = "In Defense of Program Testing or Correctness Proofs Considered Harmful", + journal = "SIGPLAN Notices", + volume = "11", + number = "1", + year = "1976", + pages = "64-68", + paper = "Tane76.pdf", + abstract = "Dijkstra's remark to the effect that testing can only + demonstrate the presence of errors and not their absence is + unquestionably true. This observation, together with the recent + development of techniques for formally proving programs to be correct, + has led some computer scientists to believe that correctness proofs + can replace testing as a means for insuring that programs do what + they are supposed to do. The purpose of this note is to point out + several reasons why even programs rigorously proven to be correct + should be neertheless thoroughly tested. Correctness proofs can + supplement, but cannot replace comprehensive testing." +} +\end{chunk} \index{Th\'ery, Laurent} \begin{chunk}{axiom.bib} @@ -16509,6 +16532,16 @@ Math. Tables Aids Comput. 10 91--96. (1956) \end{chunk} +\begin{chunk}{ignore} +@misc{Knut15, + author = "Unknown", + title = "Knuth & Plass line-breaking Revisited", + year = "2015", + url = "http://defoe.sourceforge.net/folio/knuth-plass.html" +} + +\end{chunk} + \eject %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \chapter{Bibliography} diff --git a/changelog b/changelog index 3016e45..5b048bb 100644 --- a/changelog +++ b/changelog @@ -1,3 +1,5 @@ +20150830 tpd src/axiom-website/patches.html 20150830.01.tpd.patch +20150830 tpd books/bookvolbib add Tanenbaum, Knuth references 20150828 tpd src/axiom-website/patches.html 20150828.01.tpd.patch 20150828 tpd books/bookvol10.4 add signatures to all package functions 20150815 tpd src/axiom-website/patches.html 20150815.01.tpd.patch diff --git a/patch b/patch index cbdedf0..07486a1 100644 --- a/patch +++ b/patch @@ -1,6 +1,33 @@ -books/bookvol10.4 add signatures to all package functions +books/bookvolbib add Tanenbaum, Knuth references Goal: Proving Axiom Correct -For every function in the packages add the signature of the function -to the COQ extract. +@article{Tane76, + author = "Tanenbaum, Andrew S.", + title = "In Defense of Program Testing or Correctness Proofs Considered Harmf journal = "SIGPLAN Notices", + volume = "11", + number = "1", + year = "1976", + pages = "64-68", + paper = "Tane76.pdf", + abstract = "Dijkstra's remark to the effect that testing can only + demonstrate the presence of errors and not their absence is + unquestionably true. This observation, together with the recent + development of techniques for formally proving programs to be correct, + has led some computer scientists to believe that correctness proofs + + can replace testing as a means for insuring that programs do what + they are supposed to do. The purpose of this note is to point out + several reasons why even programs rigorously proven to be correct + should be neertheless thoroughly tested. Correctness proofs can + supplement, but cannot replace comprehensive testing." +} + +@misc{Knut15, + author = "Unknown", + title = "Knuth & Plass line-breaking Revisited", + year = "2015", + url = "http://defoe.sourceforge.net/folio/knuth-plass.html" +} + + diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html index 19c8369..c8ce761 100644 --- a/src/axiom-website/patches.html +++ b/src/axiom-website/patches.html @@ -5120,6 +5120,8 @@ buglist bug 7303: Duplicate signature in )show ALIST
books/bookvol10.* extract code for COQ proof system
20150828.01.tpd.patch books/bookvol10.4 add signatures to all package functions
+20150830.01.tpd.patch +books/bookvolbib add Tanenbaum, Knuth references
-- 1.7.5.4