source: src/common/Measurable.ma

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @2914   8 years campbell Use single definition for stack measurement.
(edit) @2896   8 years campbell Complete part of measurable to structured subtraces proof that shows …
(edit) @2800   8 years campbell Tidy up Measurable.ma a little, get rid of obsolete comments.
(edit) @2795   8 years sacerdot Added new function Measurable.observe_all_in_measurable to be used to …
(edit) @2756   8 years sacerdot WARNING: this commit breaks things, sorry, Paolo is going to fix …
(edit) @2727   8 years campbell Remove a couple of redundant hypotheses.
(edit) @2725   8 years campbell Add observables to FEMeasurable proof; fix silly typo.
(edit) @2722   8 years campbell It's easier to keep the real function identifier in front-end …
(edit) @2685   8 years campbell Progress on measurable trace preservation: prefix preserves observable …
(edit) @2670   8 years campbell Clean up from recent commits.
(edit) @2669   8 years campbell Tweak exec_steps output; show that simulations extend to measurable …
(edit) @2668   8 years campbell Intermediate measurable proof check-in before I change its traces again.
(edit) @2618   8 years campbell Tidy up measurable a little.
(edit) @2617   8 years campbell Trivial simplification on split_trace.
(edit) @2596   8 years campbell Use a simpler stack cost map, and then specialise to each semantics.
(edit) @2534   8 years campbell Tweak measurable definition to stop at the return from a function.
(edit) @2511   8 years campbell Conjecture main Cminor/RTLabs simulation results. Add a few notes …
(edit) @2502   8 years campbell Sketch a little about how measurable traces might work with RTLabs and …
(add) @2486   8 years campbell First go at a generalised version of measurable.
Note: See TracRevisionLog for help on using the revision log.