Changeset 2511


Ignore:
Timestamp:
Nov 30, 2012, 6:31:29 PM (7 years ago)
Author:
campbell
Message:

Conjecture main Cminor/RTLabs simulation results.
Add a few notes about measurable traces.

Location:
src
Files:
1 added
3 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/MeasurableTraces.ma

    r2502 r2511  
    1313(* The start and end states are existentially quantified because the states
    1414   need to be extended with the shadow stack of functions.  (I'm not sure that
    15    was such a great idea now...) *)
     15   was such a great idea now...)  In principle the quantified away part of the
     16   stack would be important for stack-space correctness, except that the
     17   structured trace will never touch it, only the suffix of the trace will.
     18   We could extract the true value from the execution of the prefix anyway. *)
    1619
    1720(* XXX: split of observables seem arbitrary *)
  • src/RTLabs/abstract.ma

    r2499 r2511  
    44
    55definition RTLabs_state ≝ state.
    6 
     6definition RTLabs_genv ≝ genv.
    77
    88(* Build a full abstract status record that can be used with structured traces. *)
  • src/common/Measurable.ma

    r2502 r2511  
    7373}.
    7474
     75(* FIXME: this definition is unreasonable because it presumes we can easily
     76   identify the change in stack usage from return states, but that information
     77   is rather implicit (we only really record the function called in the
     78   extended RTLabs states when building the structured traces). *)
     79
    7580definition measurable : ∀C:preclassified_system.
    7681  ∀p:program ?? C. nat → nat →
Note: See TracChangeset for help on using the changeset viewer.