source: src/correctness.ma @ 2003

Last change on this file since 2003 was 2003, checked in by campbell, 7 years ago

Some discussion of correctness statements.

File size: 1.3 KB
Line 
1
2include "compiler.ma".
3
4include "common/SmallstepExec.ma".
5include "Clight/Cexec.ma".
6include "ASM/Interpret2.ma".
7
8(* TODO
9
10∀input_program.
11! 〈object_code,costlabel_map,labelled,cost_map〉 ← compile input_program
12
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
18
19
20
21
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 ])).
39
40
41
42What is ≃l?  Must show that "labelled" does everything that
43"input_program" does, without getting lost in some
44non-terminating loop part way.
45
46*)
47
Note: See TracBrowser for help on using the repository browser.