Last change
on this file since 1513 was
1332,
checked in by campbell, 9 years ago

Summation example updated (needs computational K).

File size:
936 bytes

Rev  Line  

[1226]  1  include "Clight/test/sum.c.ma". 

 2  

 3  example exec: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec myprog 1000 [ ]). 

 4  normalize (* you can examine the result here *) 

 5  @refl 

 6  qed. 

 7  

 8  include "Clight/SimplifyCasts.ma". 

 9  

 10  example es: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec (simplify_program myprog) 1000 [ ]). 

 11  normalize (* you can examine the result here *) 

 12  @refl 

 13  qed. 

 14  

 15  include "Clight/toCminor.ma". 

 16  include "Cminor/semantics.ma". 

 17  

[1332]  18  example 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 [ ])). 

[1226]  21  normalize 

 22  @refl 

 23  qed. 

 24  

 25  include "Cminor/toRTLabs.ma". 

 26  include "RTLabs/semantics.ma". 

 27  

 28  example e2: finishes_with (repr I32 74) ? ( 

[1332]  29  bind ? (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 [ ]))). 

[1226]  32  normalize 

 33  @refl 

 34  qed. 

Note: See
TracBrowser
for help on using the repository browser.