Changeset 12 for Csemantics/README
 Timestamp:
 Jul 7, 2010, 6:46:46 PM (11 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/README
r9 r12 2 2 ================================================= 3 3 4 Last seen working with matita svn r10877 with the patch at the bottom of this 5 file. 4 Last seen working with matita svn r10890. 6 5 7 6  Most of the memory model has been ported (common/Mem.v > Mem.ma). … … 28 27 29 28  Some of the machine integers (i.e., integers modulo) results are 30 given as axioms in Integers.ma. Implementing them could be31 difficult if we keep using a unary representation of integers as32 formalisation involves constants like 2^32.29 given as axioms in Integers.ma. Implementing them should be routine now that 30 we have a binary representation of integers. The CompCert version is given 31 as a functor on the word size  we don't have an equivalent of this yet. 33 32 34 33 * Some experimental work on an executable semantics has been started in … … 67 66 AST.ma 68 67 69 No concrete type for ident.70 68 Program transformation sections left alone. 71 69 … … 73 71 74 72 Only essential parts: 75  "align" is axiomatised 73  align 74  some 2^n lemmas (which could go into the binary libraries) 76 75  option_map 77 76  parts of list disjointness and nonrepetition … … 116 115 Mem.ma 117 116 118 Everything except for omega in proofs. 117 Everything except for omega in proofs. Much of the transformations sections 118 are commented out until Integers.ma is done properly. 119 119 120 120 Smallstep.ma … … 130 130 131 131 132 133 134 Index: matita/nlibrary/arithmetics/Z.ma135 ===================================================================136  matita/nlibrary/arithmetics/Z.ma (revision 10877)137 +++ matita/nlibrary/arithmetics/Z.ma (working copy)138 @@ 13,6 +13,7 @@139 (**************************************************************************)140 141 include "arithmetics/nat.ma".142 +include "arithmetics/compare.ma".143 144 ninductive Z : Type %Gâ%@145 OZ : Z146 @@ 508,7 +509,7 @@147 ##[//148 ###n;nrewrite < (Zsucc_Zplus_pos_O ?);nrewrite > (Zsucc_Zpred ?);//149 ##//]150 ##ncases y;//151 +##ncases y;/2/152 ##ncases y153 ##[#n;nrewrite < (sym_Zplus ??);nrewrite < (sym_Zplus (Zpred OZ) ?);154 nrewrite < (Zpred_Zplus_neg_O ?);nrewrite > (Zpred_Zsucc ?);//
Note: See TracChangeset
for help on using the changeset viewer.