Changeset 2004


Ignore:
Timestamp:
May 28, 2012, 2:35:19 PM (5 years ago)
Author:
campbell
Message:

Minor edits from discussion.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/correctness.ma

    r2003 r2004  
    1515
    1616
    17 exec_inf … clight_fullexec labelled ≈ exec_inf … ASM_fullexec output
     17exec_inf … clight_fullexec labelled ≈ exec_inf … ASM_fullexec object_code
     18(* Should we be lifting labels in some way here? *)
    1819
    1920
     
    2223∀i,f : clight_status.  [i,f labelled, at same level]
    2324i clight~> f →
    24 ∃!i',f'. i ≃ i' ∧ f ≃ f' ∧ i' asm~> f' ∧
     25∃!i',f'. i ≃ i' ∧ f ≃ f' ∧ i' 8051~> f' ∧
    2526  clock f - clock i = clock f' - clock i'.
    2627
Note: See TracChangeset for help on using the changeset viewer.