source: C-semantics/test/trivial.ma @ 3

Last change on this file since 3 was 3, checked in by campbell, 10 years ago

Import work-in-progress port of the CompCert? C semantics to matita.

File size: 936 bytes
Line 
1
2include "Csyntax.ma".
3include "Csem.ma".
4
5naxiom main : ident.
6naxiom ident_eq_eq: ∀i. ident_eq i i = inl ?? (refl ? i).
7
8ndefinition trivial : program.
9@ [ 〈main, Internal ?〉 ] main [];
10@ (Tint I32 Signed) [ ] [ ] (Sreturn (Some ??));
11@ ? (Tint I32 Signed); napply (Econst_int zero);
12nqed.
13
14nremark trivial_behaves : ∃behaviour. exec_program trivial behaviour.
15@; ##[ ##2:
16  napply program_terminates;
17  ##[ ##5: @; (* initial state *)
18    ##[ ##3: nnormalize; nrewrite > (ident_eq_eq ?); //;
19    ##| ##4: nnormalize; //;
20    ##| ##*: ##skip
21    ##]
22  ##| ##6:
23    @2; ##[ ##4: napply step_internal_function;
24          ##[ ##4: //;  ##| ##5: //; ##| ##*: ##skip ##]
25        ##| ##5: @2;
26          ##[ ##4: napply step_return_1; //; napply nmk; #H; ndestruct;
27          ##| ##5: @1;
28          ##| ##6: //;
29          ##| ##*: ##skip ##]
30        ##| ##6: //;
31        ##| ##*: ##skip
32        ##]
33  ##| ##7: @;
34  ##]
35##] nqed.
36
Note: See TracBrowser for help on using the repository browser.