Changeset 2597 for src/Cminor/toRTLabsCorrectness.ma
- Timestamp:
- Jan 31, 2013, 12:07:02 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Cminor/toRTLabsCorrectness.ma
r2511 r2597 2 2 include "Cminor/abstract.ma". 3 3 include "RTLabs/abstract.ma". 4 include "Cminor/toRTLabs.ma". 4 5 5 6 record cminor_rtlabs_inv : Type[0] ≝ { … … 68 69 cminor_rtlabs_rel INV s2 s2' 69 70 ). 71 72 (* Note that we start from the "no initialisation" version of the Cminor 73 semantics. I plan to prove the initialisation generation separately. *) 74 75 axiom cminor_noinit_rtlabs_init : ∀cm_program,ra_program,s,s'. 76 cminor_noinit_to_rtlabs cm_program = ra_program → 77 make_initial_state ?? Cminor_noinit_fullexec cm_program = OK ? s → 78 make_initial_state ?? RTLabs_fullexec ra_program = OK ? s' → 79 ∃INV. cminor_rtlabs_rel INV s s'. 80
Note: See TracChangeset
for help on using the changeset viewer.