Changeset 2875 for src/correctness.ma


Ignore:
Timestamp:
Mar 15, 2013, 1:32:50 AM (7 years ago)
Author:
sacerdot
Message:

Pretty printing of object code integrated too.
A couple of axioms make execution via the preclassified_system
raise assert false.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/correctness.ma

    r2852 r2875  
    109109  ∃n1,n2.
    110110   observables Clight_pcs (c_labelled_clight … p) m1 m2 =
    111    observables (OC_preclassified_system (c_labelled_object_code … p)) it n1 n2
     111   observables (OC_preclassified_system (c_labelled_object_code … p))
     112    (c_labelled_object_code … p) n1 n2
    112113  ∧
    113114   minus c2 c1 = clock … (execute n2 ? initial_status) - clock … (execute n1 ? initial_status).
Note: See TracChangeset for help on using the changeset viewer.