source: etc/campbell/dev-notes/2013-02-19-single-source-step-simulations.txt

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

Switch to single source step simulations for front-end measurable subtraces

File size: 1.3 KB
1I was trying a slightly unusual simulation statement where I matched up n source
2steps with m target steps, but we're reverting to the normal 1 source step to m
3target steps with a measure on source states to preserve termination.
5The simple part of the reason is that we would need to deal with the source
6program going wrong - i.e., the simulation result would either have to prove
7that the simulation happens, or that it knows some number of steps that would
8make the execution go wrong.
10Alternatively, you could provide a hypothesis saying that it doesn't go wrong,
11but then you might trouble with the measurable subtraces because you need to
12carry it around as an extra hypothesis for the measurable results (the witness
13to going wrong might be *after* the section of the trace you are interested
14in, unless you impose other troublesome constraints about hitting a labelled
17Thinking about these a little, the reasoning that's required is much the same
18as the single step version, except that you've more to keep track of.  And the
19single step version provides a more precise characterisation of the transformed
20code: even if the source program goes wrong the target code won't go wrong until
21it has performed the earlier steps corresponding to the source, including all of
22the observable events.
Note: See TracBrowser for help on using the repository browser.