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

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