Changeset 3138 for Deliverables/D3.4/Report/report.tex

Timestamp:

Apr 12, 2013, 7:03:35 PM (8 years ago)

Author:

campbell

Message:

Sketch up-to-labelling bit.

File:

• Deliverables/D3.4/Report/report.tex (modified) (1 diff)

Deliverables/D3.4/Report/report.tex

@@ -417 +417 @@
 \section{Input code to cost labelled program}
 
+The simple form of labelling used in the formalised compiler is not
+quite capable of capturing costs arising from complex C
+\lstinline[language=C]'switch' statements, largely due to the
+fall-through behaviour.  Our first pass replaces these statements with
+simpler C code, allowing our second pass to perform the cost
+labelling.  We show that the behaviour of programs is unchanged by
+these passes.
+
+TODO: both give one-step-sim-by-many forward sim results; switch
+removal tricky, uses aux var to keep result of expr, not central to
+intensional correctness so curtailed proof effort once reasonable
+level of confidence in code gained; labelling much simpler; don't care
+what the labels are at this stage, just need to know when to go
+through extra steps.  Rolled up into a single result with a cofixpoint
+to obtain coinductive statement of equivalence (show).
+
 \section{Finding corresponding measurable subtraces}