source: Deliverables/D4.1/Matita/DoTest.ma @ 360

Last change on this file since 360 was 360, checked in by sacerdot, 9 years ago

Missing include added.

File size: 982 bytes
Line 
1include "Test.ma".
2include "Interpret.ma".
3include "Assembly.ma".
4
5ndefinition testmem ≝ assembly test.
6ndefinition teststatus ≝ load testmem initialise_status.
7ndefinition testfinal ≝ execute one teststatus.
8
9notation "'STATUS'" with precedence 90 for @{ 'status }.
10interpretation "status" 'status = (mk_Status ??????????).
11
12(*
13nlemma xoo: testfinal = testfinal.
14 nnormalize in ⊢ (??%?); @;
15nqed.
16*)
17
18(*
19nlemma test:
20 (let status ≝
21 load
22  (assembly [LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;true;false;false;false]])])
23   initialise_status
24  in
25   fetch (code_memory status) (program_counter status)
26  ) = ?.
27##[ nnormalize in ⊢ (??%?);
28*)
29
30
31nlemma xoo:
32 fetch (code_memory testfinal) (program_counter testfinal) =
33 fetch (code_memory testfinal) (program_counter testfinal).
34 nnormalize in ⊢ (??%?); @;
35nqed.
36*)
37
38nlemma xoo: program_counter testfinal = program_counter testfinal.
39 nnormalize in ⊢ (??%?); @;
40nqed.
Note: See TracBrowser for help on using the repository browser.