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

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

...

File size: 1020 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 six 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
30nlemma xoo:
31 first … (first … (fetch (code_memory testfinal) (program_counter testfinal))) =
32 first … (first … (fetch (code_memory testfinal) (program_counter testfinal))).
33 nnormalize in ⊢ (??%?);
34nqed.
35
36nlemma xoo: program_counter testfinal = program_counter testfinal.
37 nnormalize in ⊢ (??%?);
38nqed.
Note: See TracBrowser for help on using the repository browser.