Changeset 2597 for src/Cminor


Ignore:
Timestamp:
Jan 31, 2013, 12:07:02 PM (7 years ago)
Author:
campbell
Message:

Some work in progress on measurable subtrace preservation.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabsCorrectness.ma

    r2511 r2597  
    22include "Cminor/abstract.ma".
    33include "RTLabs/abstract.ma".
     4include "Cminor/toRTLabs.ma".
    45
    56record cminor_rtlabs_inv : Type[0] ≝ {
     
    6869    cminor_rtlabs_rel INV s2 s2'
    6970  ).
     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
     75axiom 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.