source: src/correctness.ma @ 2001

Last change on this file since 2001 was 2001, checked in by campbell, 8 years ago

Get the compiler to output more.

File size: 614 bytes
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! 〈labelled,output〉 ← 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∀___.
23Σ_{l∈|___|} F(k)(l) = δ
24→ σ_0 -obj→ σ_f
25→ clock σ_f = clock σ_0 + δ
26
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
33*)
34
Note: See TracBrowser for help on using the repository browser.