source: src/correctness.ma @ 1996

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

Work on correctness from yesterday.

File size: 364 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! output ← compile input_program
12
13exec_inf … clight_fullexec input_program ≈ exec_inf … ASM_fullexec output
14
15
16
17
18∀___.
19Σ_{l∈|___|} F(k)(l) = δ
20→ σ_0 -obj→ σ_f
21→ clock σ_f = clock σ_0 + δ
22
23*)
24
Note: See TracBrowser for help on using the repository browser.