Changeset 1332


Ignore:
Timestamp:
Oct 10, 2011, 12:41:50 PM (8 years ago)
Author:
campbell
Message:

Summation example updated (needs computational K).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/test/sum.test.ma

    r1226 r1332  
    1616include "Cminor/semantics.ma".
    1717
    18 example e1: finishes_with (repr I32 74) ? (do p ← clight_to_cminor (simplify_program myprog); exec_up_to Cminor_fullexec p 1000 [ ]).
     18example e1: finishes_with (repr I32 74) ?
     19  (bind ? (snapshot state) (clight_to_cminor (simplify_program myprog))
     20   (λp. exec_up_to Cminor_fullexec p 1000 [ ])).
    1921normalize
    2022@refl
     
    2527
    2628example e2: finishes_with (repr I32 74) ? (
    27 do p1 ← clight_to_cminor (simplify_program myprog);
    28 do p2 ← cminor_to_rtlabs p1;
    29  exec_up_to RTLabs_fullexec p2 1000 [ ]).
     29bind ? (snapshot state) (clight_to_cminor (simplify_program myprog))
     30(λp1. bind ? (snapshot state) (cminor_to_rtlabs p1)
     31 (λp2. exec_up_to RTLabs_fullexec p2 1000 [ ]))).
    3032normalize
    3133@refl
Note: See TracChangeset for help on using the changeset viewer.