Changeset 768


Ignore:
Timestamp:
Apr 22, 2011, 1:49:12 PM (9 years ago)
Author:
campbell
Message:

Make Cminor tests test translation to RTLabs.

Location:
src/Cminor/test
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/test/factorial.ma

    r751 r768  
    7777normalize  (* you can examine the result here *)
    7878@refl qed.
     79
     80include "Cminor/toRTLabs.ma".
     81include "RTLabs/semantics.ma".
     82
     83example execRTL: finishes_with (repr 120) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [EVint (repr 5)]).
     84normalize  (* you can examine the result here *)
     85@refl
     86qed.
     87
  • src/Cminor/test/search.ma

    r751 r768  
    149149   normalize  (* you can examine the result here *)
    150150   @refl qed.
     151
     152
     153include "Cminor/toRTLabs.ma".
     154include "RTLabs/semantics.ma".
     155
     156example execRTL: finishes_with (repr 3) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [ ]).
     157normalize  (* you can examine the result here *)
     158@refl
     159qed.
     160
  • src/Cminor/test/sum.ma

    r758 r768  
    8181@refl
    8282qed.
     83
     84include "Cminor/toRTLabs.ma".
     85include "RTLabs/semantics.ma".
     86
     87example execRTL: finishes_with (repr 74) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [ ]).
     88normalize  (* you can examine the result here *)
     89@refl
     90qed.
Note: See TracChangeset for help on using the changeset viewer.