Changeset 2003


Ignore:
Timestamp:
May 28, 2012, 1:10:50 PM (5 years ago)
Author:
campbell
Message:

Some discussion of correctness statements.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/correctness.ma

    r2001 r2003  
    99
    1010∀input_program.
    11 ! 〈labelled,output〉 ← compile input_program
     11! 〈object_code,costlabel_map,labelled,cost_map〉 ← compile input_program
    1212
    1313exec_inf … clight_fullexec input_program ≃l exec_inf … clight_fullexec labelled
     
    2020
    2121
    22 ∀___.
    23 Σ_{l∈|___|} F(k)(l) = δ
    24 → σ_0 -obj→ σ_f
    25 → clock σ_f = clock σ_0 + δ
     22∀i,f : clight_status.  [i,f labelled, at same level]
     23i clight~> f →
     24∃!i',f'. i ≃ i' ∧ f ≃ f' ∧ i' asm~> f' ∧
     25  clock f - clock i = clock f' - clock i'.
     26
     27
     28∀s,flat.
     29let ge ≝ (globalenvs … labelled) in
     30subtrace_of (exec_inf … RTLabs_fullexec labelled) flat →
     31RTLabs_cost s = true →
     32∀WR : will_return ge 0 s flat.
     33let structured_trace_rtlabs ≝ make_label_return' ge 0 s flat ??? WR in
     34let labels_rtlabs ≝ flat_label_trace … flat WR in
     35∃!initial,final,structured_trace_asm.
     36  structured_trace_rtlabs ≈ structured_trace_asm ∧ 
     37  clock … code_memory … final = clock … code_memory … initial +
     38     (Σ_{i < |labels_rtlabs|} (cost_map (match nth i labels_rtlabs with [ Some k ⇒ k | None ⇒ 0 ])).
    2639
    2740
Note: See TracChangeset for help on using the changeset viewer.