source: src/common/SmallstepExec.ma

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @2685   7 years campbell Progress on measurable trace preservation: prefix preserves observable …
(edit) @2682   7 years campbell Don't apply inv in after_n_steps to last state.
(edit) @2669   7 years campbell Tweak exec_steps output; show that simulations extend to measurable …
(edit) @2668   7 years campbell Intermediate measurable proof check-in before I change its traces again.
(edit) @2618   7 years campbell Tidy up measurable a little.
(edit) @2487   7 years campbell Set up "after_n_steps" to enforce an invariant on states.
(edit) @2459   7 years campbell Syntax update
(edit) @2444   7 years campbell Some inversion lemmas for after_n_steps for dealing with >1 source …
(edit) @2338   7 years campbell Use much nicer definition for making several steps in the labelling …
(edit) @2203   7 years campbell A general result about simulations of executions.
(edit) @2202   7 years campbell Start defining equivalent executions.
(edit) @2145   7 years campbell Cost labelling doesn't affect interaction.
(edit) @2118   7 years campbell Labelling preserves behaviour.
(edit) @1599   8 years sacerdot Start of merging of stuff into the standard library of Matita.
(edit) @1233   8 years sacerdot 1) Ported to Brian's new dependent type for fullexec 2) Universe level …
(edit) @1231   8 years campbell Change SmallstepExec? so that states can depend on global information. …
(edit) @1213   8 years sacerdot 1) New values (joint/BEValues.ma) and memory model for the back-ends …
(edit) @1181   8 years mulligan changed smallstep exec in order to remove matita bug (superposition.ml …
(edit) @797   9 years campbell Add error messages wherever the error monad is used. Sticks to …
(edit) @751   9 years campbell Initial version of the Cminor syntax and semantics.
(edit) @731   9 years campbell Common definition for animation semantics, and factor out IO definitions.
(edit) @702   9 years campbell Refine small-step executable semantics abstraction a little. Some …
(edit) @700   9 years campbell Get Clight semantics going again (except for problems CexecEquiv? that …
(copy) @695   9 years campbell Rearrange Clight files a bit - will try to make them work again soon…
copied from src/Clight/SmallstepExec.ma:
(copy) @694   9 years campbell Start moving Clight into common directory.
Note: See TracRevisionLog for help on using the revision log.