Changeset 1332 for src

Timestamp:

Oct 10, 2011, 12:41:50 PM (9 years ago)

Author:

campbell

Message:

Summation example updated (needs computational K).

File:

• src/Clight/test/sum.test.ma (modified) (2 diffs)

src/Clight/test/sum.test.ma

@@ -16 +16 @@
 include "Cminor/semantics.ma".
 
-example e1: finishes_with (repr I32 74) ? (do p ← clight_to_cminor (simplify_program myprog); exec_up_to Cminor_fullexec p 1000 [ ]).
+example e1: finishes_with (repr I32 74) ?
+  (bind ? (snapshot state) (clight_to_cminor (simplify_program myprog))
+   (λp. exec_up_to Cminor_fullexec p 1000 [ ])).
 normalize
 @refl
@@ -25 +27 @@
 
 example e2: finishes_with (repr I32 74) ? (
-do p1 ← clight_to_cminor (simplify_program myprog);
-do p2 ← cminor_to_rtlabs p1;
- exec_up_to RTLabs_fullexec p2 1000 [ ]).
+bind ? (snapshot state) (clight_to_cminor (simplify_program myprog))
+(λp1. bind ? (snapshot state) (cminor_to_rtlabs p1)
+ (λp2. exec_up_to RTLabs_fullexec p2 1000 [ ]))).
 normalize
 @refl