Changeset 404 for C-semantics


Ignore:
Timestamp:
Dec 13, 2010, 11:43:26 AM (9 years ago)
Author:
campbell
Message:

Update C-semantics README.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/README

    r400 r404  
    77  The main exception is minor arithmetic results than were proven with
    88  omega, which we hope to prove using matita's automation at some
    9   point.
     9  point.  For the C semantics deliverable these (unnecessary) properties
     10  have been commented out.
    1011
    1112- The memory model is executable; some small tests can be found in
     
    2526  as a functor on the word size - we don't have an equivalent of this yet.
    2627
    27 * The executable semantics can be found in CexecIO.ma, which uses the
    28   resumption monad defined in IOMonad.ma.
     28* The executable semantics can be found in Cexec.ma, which uses the
     29  error monad in Errors.ma and the resumption monad defined in IOMonad.ma.
    2930
    3031* The patch in acc-0.1.spaces.patch adds a -ma option to the prototype
     
    8081  Program transformation sections mostly left alone.
    8182
     83CexecComplete.ma  [new]
     84
     85  Completeness of steps of executable semantics wrt inductive
     86
     87CexecEquiv.ma  [new]
     88
     89  Equivalence of complete executions to inductive semantics
     90
     91Cexec.ma  [new]
     92
     93  Definition of executable semantics
     94
     95CexecSound.ma
     96
     97  Soundness of individual steps of executable semantics wrt inductive
     98
    8299Coqlib.ma
    83100
     
    87104  - option_map
    88105  - parts of list disjointness and non-repetition
     106
     107CostLabel.ma  [new]
     108
     109  Definition of cost labels
    89110
    90111Csem.ma
     
    106127  Most of the definitions; haven't needed many of the lemmas yet.
    107128
     129extralib.ma  [new]
     130
     131  Definitions which probably belong in the matita libraries, if anywhere.
     132
    108133Floats.ma
    109134
     
    122147  in range.  The use of the Coq module system to abstract over the word size
    123148  has been left out for now.
     149
     150IOMonad.ma  [new]
     151
     152  Definition and properties of the resumption+error monad for I/O.
    124153
    125154Maps.ma
Note: See TracChangeset for help on using the changeset viewer.