Line | |
---|
1 | include "Test.ma". |
---|
2 | include "Interpret.ma". |
---|
3 | |
---|
4 | ndefinition testmem ≝ assembly test. |
---|
5 | ndefinition teststatus ≝ load testmem initialise_status. |
---|
6 | ndefinition testfinal ≝ execute one teststatus. |
---|
7 | |
---|
8 | notation "'STATUS'" with precedence 90 for @{ 'status }. |
---|
9 | interpretation "status" 'status = (mk_Status ??????????). |
---|
10 | |
---|
11 | (* |
---|
12 | nlemma xoo: testfinal = testfinal. |
---|
13 | nnormalize in ⊢ (??%?); @; |
---|
14 | nqed. |
---|
15 | *) |
---|
16 | |
---|
17 | (* |
---|
18 | nlemma 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 | |
---|
30 | nlemma xoo: |
---|
31 | fetch (code_memory testfinal) (program_counter testfinal) = |
---|
32 | fetch (code_memory testfinal) (program_counter testfinal). |
---|
33 | nnormalize in ⊢ (??%?); @; |
---|
34 | nqed. |
---|
35 | *) |
---|
36 | |
---|
37 | nlemma xoo: program_counter testfinal = program_counter testfinal. |
---|
38 | nnormalize in ⊢ (??%?); @; |
---|
39 | nqed. |
---|
Note: See
TracBrowser
for help on using the repository browser.