Changeset 2003
- Timestamp:
- May 28, 2012, 1:10:50 PM (6 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/correctness.ma
r2001 r2003 9 9 10 10 ∀input_program. 11 ! 〈 labelled,output〉 ← compile input_program11 ! 〈object_code,costlabel_map,labelled,cost_map〉 ← compile input_program 12 12 13 13 exec_inf … clight_fullexec input_program ≃l exec_inf … clight_fullexec labelled … … 20 20 21 21 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] 23 i 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. 29 let ge ≝ (globalenvs … labelled) in 30 subtrace_of (exec_inf … RTLabs_fullexec labelled) flat → 31 RTLabs_cost s = true → 32 ∀WR : will_return ge 0 s flat. 33 let structured_trace_rtlabs ≝ make_label_return' ge 0 s flat ??? WR in 34 let 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 ])). 26 39 27 40
Note: See TracChangeset
for help on using the changeset viewer.