source: etc/campbell/dev-notes/2011-08-25-cminor-labels.txt

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

I've kept the odd note on bits of CerCo? work I've been doing. James suggested
that it might be useful if these were recorded in the repository just in case
they contain some useful information that doesn't get recorded elsewhere.

File size: 1.0 KB
1While looking at removing the unnecessary sources of failure in the Cminor
2semantics I'd like to stop the function to find goto-labels in the function
3body from failing.  However, this function performs a search of the entire
4body, so we can't just pass the invariant in because it *ought* to fail for
5the statements which don't contain the label.
7Three possibilities come to mind:
91. prove separately that a search on the entire function body will succeed by
10   exhausting the possibilities for the label invariant to be true,
112. build a label to statement map instead, keep proof that it's ok, or
123. put in paths to the label and a proof that they're correct.
14The translation to RTLabs doesn't have this problem as it constructs a fresh
15label mapping, then maintain the invariant that all labels defined in a
16statement that has been translated have a counterpart in the graph.  1 neither
17requires or suggests any changes to this; 2 just makes us use the keys of the
18map instead of the list of labels in the body; 3 similarly.  Hence 1 is the
19most straightforward.
Note: See TracBrowser for help on using the repository browser.