source: Deliverables/D4.1/Matita/Test.ma @ 346

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

An example of execution.

File size: 7.5 KB
Line 
1(*include "Interpret.ma".*)
2include "Assembly.ma".
3include "Status.ma".
4
5ndefinition test: List instruction ≝
6 [LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;true;false;false;false]]);
7  LCALL … (ADDR16 [[false;false;false;false;false;false;false;false;false;true;true;false;false;true;false;false]]);
8  SJMP … (RELATIVE [[true;true;true;true;true;true;true;false]]);
9  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;false;true]]),(DATA [[false;false;false;false;false;true;true;true]])〉))));
10  LCALL … (ADDR16 [[false;false;false;false;false;false;false;false;false;true;true;false;true;true;true;false]]);
11  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[true;false;false;false;false;false;true;false]])〉)))));
12  Jump … (JZ … (RELATIVE [[false;false;false;false;false;false;true;true]]));
13  LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;true;true]]);
14  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
15  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;true]])〉)))));
16  ORL … (Left … (Left … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
17  Jump … (JZ … (RELATIVE [[false;false;false;true;true;false;true;true]]));
18  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
19  MOV … (Left … (Left … (Right … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;true;true;true;false;false;true;false]])〉)));
20  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
21  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
22  CLR … (ACC_A);
23  MOVC … (ACC_A) (ACC_DPTR);
24  MOVX … (Right … 〈(EXT_INDIRECT false),(ACC_A)〉);
25  INC … (DPTR);
26  INC … (REGISTER [[false;false;false]]);
27  Jump … (CJNE … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉) (RELATIVE [[false;false;false;false;false;false;true;false]]));
28  INC … (DIRECT [[true;false;true;false;false;false;false;false]]);
29  Jump … (DJNZ … (REGISTER [[false;false;true]]) (RELATIVE [[true;true;true;true;false;true;false;false]]));
30  Jump … (DJNZ … (REGISTER [[false;true;false]]) (RELATIVE [[true;true;true;true;false;false;true;false]]));
31  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉))));
32  CLR … (ACC_A);
33  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉)))));
34  MOV … (Left … (Left … (Left … (Left … (Right … 〈(INDIRECT false),(ACC_A)〉)))));
35  Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;true]]));
36  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
37  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;false]])〉)))));
38  ORL … (Left … (Left … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
39  Jump … (JZ … (RELATIVE [[false;false;false;false;true;false;true;false]]));
40  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
41  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
42  CLR … (ACC_A);
43  MOVX … (Right … 〈(EXT_INDIRECT true),(ACC_A)〉);
44  INC … (REGISTER [[false;false;true]]);
45  Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;false]]));
46  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
47  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;false]])〉)))));
48  ORL … (Left … (Left … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
49  Jump … (JZ … (RELATIVE [[false;false;false;false;true;true;false;false]]));
50  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
51  MOV … (Left … (Left … (Right … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;false;false]])〉)));
52  CLR … (ACC_A);
53  MOVX … (Right … 〈(EXT_INDIRECT_DPTR),(ACC_A)〉);
54  INC … (DPTR);
55  Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;false]]));
56  Jump … (DJNZ … (REGISTER [[false;false;true]]) (RELATIVE [[true;true;true;true;true;false;true;false]]));
57  LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;true;true]]);
58  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;true;false;true]])〉)))));
59  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;true;false;true]]),(DATA [[false;false;false;false;true;true;true;true]])〉))));
60  XCHD … (ACC_A) (INDIRECT false);
61  MOV … (Left … (Left … (Right … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;false;false]])〉)));
62  RET … ;
63  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
64  RET … ;
65  NOP … ;
66  NOP … ;
67  NOP … ;
68  NOP … ;
69  NOP … ;
70  NOP … ;
71  NOP … ;
72  NOP … ;
73  NOP … ;
74  NOP … ;
75  NOP … ;
76  NOP … ;
77  NOP … ;
78  NOP … ;
79  NOP … ;
80  NOP … ;
81  NOP … ;
82  NOP … ;
83  NOP … ;
84  NOP … ;
85  NOP … ;
86  NOP … ;
87  NOP … ;
88  NOP … ;
89  NOP … ;
90  NOP … ;
91  NOP … ;
92  NOP … ;
93  NOP … ;
94  NOP … ;
95  NOP … ;
96  NOP … ;
97  NOP … ;
98  NOP … ;
99  NOP … ;
100  NOP … ;
101  NOP … ;
102  NOP … ;
103  NOP … ;
104  NOP … ;
105  NOP … ;
106  NOP … ;
107  NOP … ;
108  NOP … ;
109  NOP … ;
110  NOP … ;
111  NOP … ;
112  NOP … ;
113  NOP … ;
114  NOP … ;
115  NOP … ;
116  NOP … ;
117  NOP … ;
118  NOP … ;
119  NOP … ;
120  NOP … ;
121  NOP … ;
122  NOP … ;
123  NOP … ;
124  NOP … ;
125  NOP … ;
126  NOP … ;
127  NOP … ;
128  NOP … ;
129  NOP … ;
130  NOP … ;
131  NOP … ;
132  NOP … ;
133  NOP … ;
134  NOP … ;
135  NOP … ;
136  NOP … ;
137  NOP … ;
138  NOP … ;
139  NOP … ;
140  NOP … ;
141  NOP … ;
142  NOP … ;
143  NOP … ;
144  NOP … ;
145  NOP … ;
146  NOP … ;
147  NOP … ;
148  NOP … ;
149  NOP … ;
150  NOP … ;
151  NOP … ].
152 @.
153nqed.
154
155ndefinition testmem ≝ assembly test.
156
157nlemma foo: testmem = testmem.
158 nnormalize; @.
159nqed.
160
161ndefinition teststatus ≝ load testmem initialise_status.
162
163nlemma goo: teststatus = teststatus.
164 nnormalize; @.
165nqed.
Note: See TracBrowser for help on using the repository browser.