Changeset 12
- Timestamp:
- Jul 7, 2010, 6:46:46 PM (11 years ago)
- Location:
- C-semantics
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
C-semantics/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 non-repetition … … 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 ?);// -
C-semantics/test/memorymodel.ma
r3 r12 24 24 ndefinition store1 : mem ≝ fst ?? store1block. 25 25 ndefinition block := snd ?? store1block. 26 26 27 (* write a value *) 27 28 ndefinition store2 : mem. 28 29 nletin r ≝ (store Mint16unsigned store1 block 0 (Vint one)); 30 29 31 nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct; 30 32 ##| #rr; #_; napply rr ##] nqed. 33 31 34 (* overwrite the first byte of the value *) 32 35 ndefinition store3 : mem. 33 36 nletin r ≝ (store Mint8unsigned store1 block 0 (Vint one)); 37 34 38 nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct; 35 39 ##| #rr; #_; napply rr ##] nqed. 36 40 37 ndefinition vl := load Mint16signed store3 block 0.38 41 (* The size checking rejects the read and gives us Some Vundef. *) 39 nremark vl_undef: vl= Some ? Vundef. //; nqed.42 nremark vl_undef: load Mint16signed store3 block 0 = Some ? Vundef. //; nqed. 40 43 41 ndefinition vl' := load Mint8unsigned store3 block 0.42 44 (* The read is successful and returns a signed version of the value. *) 43 nremark vl_ok': vl'= Some ? (Vint (zero_ext 8 one)). //; nqed.45 nremark vl_ok': load Mint8unsigned store3 block 0 = Some ? (Vint (zero_ext 8 one)). //; nqed. 44 46 45 ndefinition store4 := free store3 block.46 47 (* NB: Double frees are allowed by the memory model (although not necessarily 47 48 by the language). *) 49 ndefinition store4 := free store3 block. 48 50 ndefinition store5 : mem. nletin r ≝ (free store3 block); nwhd in r; napply r; nqed. 49 51
Note: See TracChangeset
for help on using the changeset viewer.