From cbe95e99fd6657fa6c8e77478b6d726fe65d4889 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Tue, 4 Apr 2017 19:10:08 0400
Subject: [PATCH] books/bookvol10.3 Add unittest and help for PrimeField
Goal: Axiom Literate Programming

books/bookvol10.3.pamphlet  70 +++++++++++++++++++++++
changelog  2 +
patch  119 +
src/axiomwebsite/patches.html  2 +
4 files changed, 75 insertions(+), 118 deletions()
diff git a/books/bookvol10.3.pamphlet b/books/bookvol10.3.pamphlet
index cc135e6..7a4df7f 100644
 a/books/bookvol10.3.pamphlet
+++ b/books/bookvol10.3.pamphlet
@@ 159805,7 +159805,7 @@ PositiveInteger() : SIG == CODE where
)set message auto off
)clear all
S 1 of 1
+S 1 of 6
)show PrimeField
R
R PrimeField(p: PositiveInteger) is a domain constructor
@@ 159898,6 +159898,50 @@ PositiveInteger() : SIG == CODE where
R
E 1
+S 2 of 6
+t1:=x^81
+R
+R
+R 8
+R (1) x  1
+R Type: Polynomial(Integer)
+E 2
+
+S 3 of 6
+factor(t1)
+R
+R
+R 2 4
+R (2) (x  1)(x + 1)(x + 1)(x + 1)
+R Type: Factored(Polynomial(Integer))
+E 3
+
+S 4 of 6
+t3:POLY(PF(3)):=t1
+R
+R
+R 8
+R (3) x + 2
+R Type: Polynomial(PrimeField(3))
+E 4
+
+S 5 of 6
+factor(t1::POLY PF 3)
+R
+R
+R 2 2 2
+R (4) (x + 1)(x + 2)(x + 1)(x + x + 2)(x + 2x + 2)
+R Type: Factored(Polynomial(PrimeField(3)))
+E 5
+
+S 6 of 6
+factor(t1::POLY PF 17)
+R
+R
+R (5) (x + 1)(x + 2)(x + 4)(x + 8)(x + 9)(x + 13)(x + 15)(x + 16)
+R Type: Factored(Polynomial(PrimeField(17)))
+E 6
+
)spool
)lisp (bye)
\end{chunk}
@@ 159910,6 +159954,30 @@ PrimeField(p) implements the field with p elements if p is a prime number.
Error: if p is not prime.
Note: this domain does not check that argument is a prime.
+ t1:=x^81
+ 8
+ x  1
+
+
+ factor(t1)
+ 2 4
+ (x  1)(x + 1)(x + 1)(x + 1)
+
+
+ t3:POLY(PF(3)):=t1
+ 8
+ x + 2
+
+
+ factor(t1::POLY PF 3)
+ 2 2 2
+ (x + 1)(x + 2)(x + 1)(x + x + 2)(x + 2x + 2)
+
+
+ factor(t1::POLY PF 17)
+ (x + 1)(x + 2)(x + 4)(x + 8)(x + 9)(x + 13)(x + 15)(x + 16)
+
+
See Also:
o )show PrimeField
diff git a/changelog b/changelog
index e88c863..53f3d00 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20170404 tpd src/axiomwebsite/patches.html 20170404.01.tpd.patch
+20170404 tpd books/bookvol10.3 Add unittest and help for PrimeField
20170403 tpd src/axiomwebsite/patches.html 20170403.01.tpd.patch
20170403 tpd books/bookvolbib add proof references
20170325 myb src/axiomwebsite/patches.html 20170325.01.myb.patch
diff git a/patch b/patch
index da4f8a0..bf6202a 100644
 a/patch
+++ b/patch
@@ 1,119 +1,4 @@
books/bookvolbib add proof references
+books/bookvol10.3 Add unittest and help for PrimeField
Goal: Proving Axiom Correct
+Goal: Axiom Literate Programming
\index{Platzer, Andre}
\index{Quesel, JanDavid}
\index{Rummer, Philipp}
\begin{chunk}{axiom.bib}
@article{Plat09,
 author = "Platzer, Andre and Quesel, JanDavid and Rummer, Philipp",
 title = "Real World Verification",
 journal = "LNCS",
 volume = "5663",
 year = "2009",
 pages = "495501",
 link = "\url{http://www.cs.cmu.edu/~aplatzer/pub/rwv.pdf}",
 abstract =
 "Scalable handling of real arithmetic is a crucial part of the
 verification of hybrid systems, mathematical algorithms, and mixed
 analog/digital circuits. Despite substantial advances in verification
 technology, complexity issues with classical decision procedures are
 still a major obstacle for formal verification of realworld
 applications, e.g., in automotive and avionic industries. To identify
 strengths and weaknesses, we examine state of the art symbolic
 techniques and implementations for the universal fragment of
 realclosed fields: approaches based on quantifier elimination,
 Groebner Bases, and semidefinite programming for the
 Positivstellensatz. Within a uniform context of the verification tool
 KeYmaera, we compare these approaches qualitatively and quantitatively
 on verification benchmarks from hybrid systems, textbook algorithms,
 and on geometric problems. Finally, we introduce a new decision
 procedure combining Groebner Bases and semidefinite programming for
 the real Nullstellensatz that outperforms the individual approaches on
 an interesting set of problems.",
 paper = "Plat09,pdf"
}

\end{chunk}

\index{Krebbers, Robbert Jan}
\index{Wiedijk, Freek}
\begin{chunk}{axiom.bib}
@misc{Kreb15a,
 author = "Krebbers, Robbert and Wiedijk, Freek",
 title = "A Typed C11 Semantics for Interactive Theorem Proving",
 year = "2015",
 link = "\url{http://robbertkrebbers.nl/research/articles/interpreter.pdf}",
 abstract =
 "We present a semantics of a significant fragment of the C programming
 language as described by the C11 standard. It consists of a small step
 semantics of a core language, which uses a structured memory model to
 capture subtleties of C11, such as strictaliasing restrictions
 related to unions, that have not yet been addressed by others. The
 semantics of actual C programs is defined by translation into this
 core language. We have an explicit type system for the core language,
 and prove type preservation and progress, as well as type correctness
 of the translation.

 Due to unspecified order of evaluation, our operational semantics is
 nondeterministic. To explore all defined and undefined behaviors, we
 present an executable semantics that computes a stream of finite sets
 of reachable states. It is proved sound and complete with respect to
 the operational semantics.

 Both the translation into the core language and the executable
 semantics are defined as Coq programs. Extraction to OCaml is used to
 obtain a C interpreter to run and test the semantics on actual C
 programs. All proofs are fully formalized in Coq.",
 paper = "Kreb15a.pdf"
}

\end{chunk}

\index{Krebbers, Robbert Jan}
\begin{chunk}{axiom.bib}
@misc{Kreb17,
 author = "Krebbers, Robbert Jan",
 title = {The CH$_2$O formalization of ISO C11},
 year = "2017",
 link = "\url{http://robbertkrebbers.nl/research/ch2o/}"
}

\end{chunk}


\index{Liskov, Barbara}
\index{Synder, Alan}
\index{Atkinson, Russell}
\index{Schaffert, Craig}
\begin{chunk}{axiom.bib}
@article{Lisk77,
 author = "Liskov, Barbara and Synder, Alan and Atkinson, Russell and
 Schaffert, Craig",
 title = "Abstraction Mechanisms in CLU",
 journal = "CACM",
 volume = "20",
 number = "8",
 year = "1977",
 link = "\url{https://www.cs.virginia.edu/~weimer/615/reading/liskovcluabstraction.pdf}",
 abstract =
 "CLU is a new programming language designed to support the use of
 abstractions in program construction. Work in programming methodology
 has led to the realization that three kinds of abstractions 
 procedural, control, and especially data abstractions  are useful in
 the programming process. Of these, only the procedural abstraction is
 supported well by conventional languages, through the procedure or
 subroutine. CLU provides, in addition to procedures, novel linguistic
 mechanisms that support the use of data and control abstractions. This
 paper provides an introduction to the abstraction mechanisms of
 CLU. By means of programming examples, the utility of the three kinds
 of abstractions in program construction is illustrated, and it is
 shown how CLU programs may be written to use and implement
 abstractions. The CLU library, which permits incremental program
 development with complete type checking performed at compile time, is
 also discussed.",
 paper = "Lisk77.pdf"
}

\end{chunk}
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index 1399d4c..9035c78 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5680,6 +5680,8 @@ books/bookvolbib Homotopy Type Theory reference
books/bookvolbib Martin Baker's PERMGRP documentation
20170403.01.tpd.patch
books/bookvolbib add proof references
+20170404.01.tpd.patch
+books/bookvol10.3 Add unittest and help for PrimeField

1.7.5.4