Index: /C-semantics/README
===================================================================
--- /C-semantics/README (revision 403)
+++ /C-semantics/README (revision 404)
@@ -7,5 +7,6 @@
The main exception is minor arithmetic results than were proven with
omega, which we hope to prove using matita's automation at some
- point.
+ point. For the C semantics deliverable these (unnecessary) properties
+ have been commented out.
- The memory model is executable; some small tests can be found in
@@ -25,6 +26,6 @@
as a functor on the word size - we don't have an equivalent of this yet.
-* The executable semantics can be found in CexecIO.ma, which uses the
- resumption monad defined in IOMonad.ma.
+* The executable semantics can be found in Cexec.ma, which uses the
+ error monad in Errors.ma and the resumption monad defined in IOMonad.ma.
* The patch in acc-0.1.spaces.patch adds a -ma option to the prototype
@@ -80,4 +81,20 @@
Program transformation sections mostly left alone.
+CexecComplete.ma [new]
+
+ Completeness of steps of executable semantics wrt inductive
+
+CexecEquiv.ma [new]
+
+ Equivalence of complete executions to inductive semantics
+
+Cexec.ma [new]
+
+ Definition of executable semantics
+
+CexecSound.ma
+
+ Soundness of individual steps of executable semantics wrt inductive
+
Coqlib.ma
@@ -87,4 +104,8 @@
- option_map
- parts of list disjointness and non-repetition
+
+CostLabel.ma [new]
+
+ Definition of cost labels
Csem.ma
@@ -106,4 +127,8 @@
Most of the definitions; haven't needed many of the lemmas yet.
+extralib.ma [new]
+
+ Definitions which probably belong in the matita libraries, if anywhere.
+
Floats.ma
@@ -122,4 +147,8 @@
in range. The use of the Coq module system to abstract over the word size
has been left out for now.
+
+IOMonad.ma [new]
+
+ Definition and properties of the resumption+error monad for I/O.
Maps.ma