|
43158
|
1 |
header "Extensions and Variations of IMP"
|
|
|
2 |
|
|
|
3 |
theory Procs imports BExp begin
|
|
|
4 |
|
|
|
5 |
subsection "Procedures and Local Variables"
|
|
|
6 |
|
|
45212
|
7 |
type_synonym pname = string
|
|
|
8 |
|
|
43158
|
9 |
datatype
|
|
|
10 |
com = SKIP
|
|
45212
|
11 |
| Assign vname aexp ("_ ::= _" [1000, 61] 61)
|
|
47818
|
12 |
| Seq com com ("_;/ _" [60, 61] 60)
|
|
43158
|
13 |
| If bexp com com ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61)
|
|
|
14 |
| While bexp com ("(WHILE _/ DO _)" [0, 61] 61)
|
|
45212
|
15 |
| Var vname com ("(1{VAR _;;/ _})")
|
|
|
16 |
| Proc pname com com ("(1{PROC _ = _;;/ _})")
|
|
|
17 |
| CALL pname
|
|
43158
|
18 |
|
|
|
19 |
definition "test_com =
|
|
|
20 |
{VAR ''x'';;
|
|
|
21 |
''x'' ::= N 0;
|
|
|
22 |
{PROC ''p'' = ''x'' ::= Plus (V ''x'') (V ''x'');;
|
|
|
23 |
{PROC ''q'' = CALL ''p'';;
|
|
|
24 |
{VAR ''x'';;
|
|
|
25 |
''x'' ::= N 5;
|
|
|
26 |
{PROC ''p'' = ''x'' ::= Plus (V ''x'') (N 1);;
|
|
|
27 |
CALL ''q''; ''y'' ::= V ''x''}}}}}"
|
|
|
28 |
|
|
|
29 |
end
|