Ignore:
Timestamp:
Apr 1, 2011, 1:35:18 PM (9 years ago)
Author:
campbell
Message:

Common definition for animation semantics, and factor out IO definitions.

File:
1 edited

Legend:

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

    r726 r731  
    1 include "Clight/Animation.ma".
     1include "Clight/Cexec.ma".
     2include "common/Animation.ma".
    23
    34definition myprog := mk_program clight_fundef type
     
    403404.
    404405
    405 example exec:
    406   (do 〈t,s〉 ← exec_up_to myprog 1000 [EVint (repr 0)]; OK ? (is_final s)) = OK ? (Some ? (repr 6)).
     406example exec: finishes_with (repr 6) ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 0)]).
    407407normalize @refl
    408408qed.
Note: See TracChangeset for help on using the changeset viewer.