Changeset 1617 for src/RTLabs

Timestamp:

Dec 14, 2011, 6:17:50 PM (8 years ago)

Author:

campbell

Message:

Note stuff to do on structured traces.

File:

• src/RTLabs/Traces.ma (modified) (1 diff)

src/RTLabs/Traces.ma

@@ -567 +567 @@
   
 (* FIXME: there's trouble at the end of the program because we can't make a step
-   away from the final return. *)
+   away from the final return.
+   
+   We need to show that the "next pc" is preserved through a function call.
+   
+   Tail-calls are not handled properly (which means that if we try to show the
+   full version with non-termination we'll fail because calls and returns aren't
+   balanced.
+   
+   The guardedness check will reject the recursive definition above; need to
+   rearrange things so that this works properly.
+ *)