Changeset 731 for src/Clight/test


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.

Location:
src/Clight/test
Files:
6 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.
  • 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.
  • src/Clight/test/insertsort.ma

    r726 r731  
    1 include "Clight/Animation.ma".
     1include "Clight/Cexec.ma".
     2include "common/Animation.ma".
    23
    34definition myprog := mk_program clight_fundef type
     
    199200
    200201example exec:
    201   (do 〈t,s〉 ← exec_up_to myprog 1000 [EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0)];
    202    OK ? t) = OK ?
     202  (do s ← exec_up_to clight_fullexec myprog 1000
     203     [EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0)];
     204   match s with [ finished t _ _ ⇒ OK ? t | _ ⇒ Error ? ]) = OK ?
    203205[EVextcall (ident_of_nat 11) [EVint (repr 36)] (EVint (repr 0));
    204206 EVextcall (ident_of_nat 11) [EVint (repr 69)] (EVint (repr 0));
  • src/Clight/test/io.ma

    r726 r731  
    1 include "Clight/Animation.ma".
     1include "Clight/Cexec.ma".
     2include "common/Animation.ma".
    23
    34definition myprog := mk_program clight_fundef type
     
    2122
    2223example exec:
    23  (do 〈t,s〉 ← exec_up_to myprog 1000 [EVint (repr 7)]; do r ← opt_to_res … (is_final s); OK ? 〈t,r〉) =
     24 (do r ← exec_up_to clight_fullexec myprog 1000 [EVint (repr 7)];
     25  match r with [ finished t r _ ⇒ OK ? 〈t,r〉 | _ ⇒ Error ? ]) =
    2426 OK ? 〈[EVextcall (ident_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 7〉.
    2527normalize  (* you can examine the result here *)
  • src/Clight/test/io2.ma

    r726 r731  
    1 include "Clight/Animation.ma".
     1include "Clight/Cexec.ma".
     2include "common/Animation.ma".
    23
    34definition myprog := mk_program clight_fundef type
     
    3031
    3132example exec:
    32  (do 〈t,s〉 ← exec_up_to myprog 1000 [EVint (repr 7)]; do r ← opt_to_res … (is_final s); OK ? 〈t,r〉) =
     33 (do r ← exec_up_to clight_fullexec myprog 1000 [EVint (repr 7)];
     34   match r with [ finished t r _ ⇒ OK ? 〈t,r〉 | _ ⇒ Error ? ]) =
    3335 OK ? 〈[EVextcall (ident_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 9〉.
    3436normalize  (* you can examine the result here *)
  • src/Clight/test/search.ma

    r726 r731  
    1 include "Clight/Animation.ma".
     1include "Clight/Cexec.ma".
     2include "common/Animation.ma".
    23
    34definition myprog := mk_program clight_fundef type
     
    188189.
    189190
    190 example exec: result ? (exec_up_to myprog 1000 [EVint (repr 0)]).
     191example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 0)]).
    191192normalize  (* you can examine the result here *)
    192193%
Note: See TracChangeset for help on using the changeset viewer.