source: etc/campbell/dev-notes/2012-04-26-label-sim.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: 612 bytes
Line 
1I was defining the labelling simulation by reference to the actual labelling
2function, i.e.,
3
4  s,k was in the relation with (\fst (label_statement s)),k'
5
6with a suitable constraint on k and k'.  However, this is a pain because of the
7threading of the name generator through the definition of label_statement, and
8more seriously because there are statements that need to be in the relation
9that are not.  For example, after  Sskip,Kwhile ...  execution should reach the
10head of the while loop again, but there are no matching states because
11
12  Swhile e s, k  only matches  Ssequence (Swhile ...) Scost ..., ...
Note: See TracBrowser for help on using the repository browser.