Changeset 2597


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

Some work in progress on measurable subtrace preservation.

Location:
src
Files:
1 added
2 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminorCorrectness.ma

    r2591 r2597  
    338338  ).
    339339
     340axiom clight_cminor_init : ∀cl_program,cm_program,s,s'.
     341  clight_to_cminor cl_program = OK ? cm_program →
     342  make_initial_state ?? clight_fullexec cl_program = OK ? s →
     343  make_initial_state ?? Cminor_fullexec cm_program = OK ? s' →
     344  ∃INV. clight_cminor_rel INV s s'.
  • 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.