source: etc/campbell/dev-notes/2012-10-30-stuttering-and-termination.txt

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

Misc notes.

File size: 718 bytes
Line 
1The usual form forward simulation (e.g., in CompCert) use an ordering / reducing
2measure on source states to argue that any translation to zero steps
3(stuttering) in the target only goes on for a finite amount of time, preserving
4non-termination.  In CerCo we might be able to avoid this if we require soundly
5cost labelled programs for the affected stages, because sound labelling requires
6that a labelled state eventually appears and we're not allowed to erase them.
7
8I think we should be able to do this generically, by demonstrating a plain n:m
9step argument (that necessarily preserves cost labels in the trace), then using
10the sound labelling when lifting the result to full executions in place of the
11ordering.
Note: See TracBrowser for help on using the repository browser.