Changeset 2001 for src/correctness.ma


Ignore:
Timestamp:
May 25, 2012, 1:47:32 PM (8 years ago)
Author:
campbell
Message:

Get the compiler to output more.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/correctness.ma

    r1996 r2001  
    99
    1010∀input_program.
    11 ! output ← compile input_program
     11! 〈labelled,output〉 ← compile input_program
    1212
    13 exec_inf … clight_fullexec input_program ≈ exec_inf … ASM_fullexec output
     13exec_inf … clight_fullexec input_program ≃l exec_inf … clight_fullexec labelled
     14
     15
     16
     17exec_inf … clight_fullexec labelled ≈ exec_inf … ASM_fullexec output
    1418
    1519
     
    2125→ clock σ_f = clock σ_0 + δ
    2226
     27
     28
     29What is ≃l?  Must show that "labelled" does everything that
     30"input_program" does, without getting lost in some
     31non-terminating loop part way.
     32
    2333*)
    2434
Note: See TracChangeset for help on using the changeset viewer.