Changeset 12 for C-semantics/README


Ignore:
Timestamp:
Jul 7, 2010, 6:46:46 PM (10 years ago)
Author:
campbell
Message:

Make memory model tests more readable.
Update README.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/README

    r9 r12  
    22=================================================
    33
    4 Last seen working with matita svn r10877 with the patch at the bottom of this
    5 file.
     4Last seen working with matita svn r10890.
    65
    76- Most of the memory model has been ported (common/Mem.v -> Mem.ma).
     
    2827
    2928- Some of the machine integers (i.e., integers modulo) results are
    30   given as axioms in Integers.ma.  Implementing them could be
    31   difficult if we keep using a unary representation of integers as
    32   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.
    3332
    3433* Some experimental work on an executable semantics has been started in
     
    6766AST.ma
    6867
    69   No concrete type for ident.
    7068  Program transformation sections left alone.
    7169
     
    7371
    7472  Only essential parts:
    75   - "align" is axiomatised
     73  - align
     74  - some 2^n lemmas (which could go into the binary libraries)
    7675  - option_map
    7776  - parts of list disjointness and non-repetition
     
    116115Mem.ma
    117116
    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.
    119119
    120120Smallstep.ma
     
    130130
    131131
    132 
    133 
    134 Index: matita/nlibrary/arithmetics/Z.ma
    135 ===================================================================
    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 : Z
    146 @@ -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 y
    153     ##[#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.