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

Last change on this file since 358 was 357, checked in by sacerdot, 10 years ago
  • stupid bug fixed in BitVectorTrie?
  • dependencies minimized, dead code removed
File size: 959 bytes
RevLine 
[355]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
[357]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
[355]30nlemma xoo:
[357]31 fetch (code_memory testfinal) (program_counter testfinal) =
32 fetch (code_memory testfinal) (program_counter testfinal).
[355]33 nnormalize in ⊢ (??%?); @;
34nqed.
[357]35*)
[355]36
37nlemma xoo: program_counter testfinal = program_counter testfinal.
38 nnormalize in ⊢ (??%?); @;
39nqed.
Note: See TracBrowser for help on using the repository browser.