Ignore:
Timestamp:
Sep 15, 2011, 2:01:56 PM (9 years ago)
Author:
sacerdot
Message:

1) New values (joint/BEValues.ma) and memory model for the back-ends

(joint/BEMem.ma) where all values are Byte-valued.

2) Improved joint semantics for the back-end languages based on the new

memory model (work in progress).

3) SmallStepExec? made more general to accomodate states with an arbitrary

memory inside.

4) New files common/Pointers.ma and common/GenMem.ma shared between the

front-end and the back-end. GenMem?.ma, at the moment, is not used in Mem.ma
(cut&paste code).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Animation.ma

    r963 r1213  
    1818inductive snapshot (state:Type[0]) : Type[0] ≝
    1919| running : trace → state → snapshot state
    20 | finished : trace → int → mem → snapshot state
     20| finished : trace → int → state → snapshot state
    2121| input_exhausted : trace → snapshot state.
    2222
     
    4848inductive snapshot' (state:Type[0]) : Type[0] ≝
    4949| running' : trace → state → snapshot' state
    50 | finished' : nat → trace → int → mem → snapshot' state
     50| finished' : nat → trace → int → state → snapshot' state
    5151| input_exhausted' : trace → snapshot' state
    5252| failed' : errmsg → nat → state → snapshot' state
     
    9595λr,S,s. match s with [ OK s' ⇒ match s' with [ finished t r' _ ⇒ r = r' | _ ⇒ False ] | _ ⇒ False ].
    9696
     97include "common/Mem.ma".
     98
    9799(* Hide the representation of memory to make displaying the results easier. *)
    98100
Note: See TracChangeset for help on using the changeset viewer.