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/factorial.ma

    r726 r731  
    1 include "Clight/Animation.ma".
     1include "Clight/Cexec.ma".
     2include "common/Animation.ma".
    23
    34definition myprog := mk_program clight_fundef type
     
    4344.
    4445
    45 example exec:
    46   (do 〈t,s〉 ← exec_up_to myprog 1000 [EVint (repr 5)]; OK ? (is_final s)) = OK ? (Some ? (repr 120)).
     46example exec: finishes_with (repr 120) ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 5)]).
    4747normalize  (* you can examine the result here *)
    4848@refl qed.
Note: See TracChangeset for help on using the changeset viewer.