46 body :: " pname ~=> com" |
46 body :: " pname ~=> com" |
47 defs body_def: "body == map_of bodies" |
47 defs body_def: "body == map_of bodies" |
48 |
48 |
49 |
49 |
50 (* Well-typedness: all procedures called must exist *) |
50 (* Well-typedness: all procedures called must exist *) |
51 consts WTs :: "com set" |
|
52 syntax WT :: "com => bool" |
|
53 translations "WT c" == "c : WTs" |
|
54 |
51 |
55 inductive WTs intros |
52 inductive WT :: "com => bool" where |
56 |
53 |
57 Skip: "WT SKIP" |
54 Skip: "WT SKIP" |
58 |
55 |
59 Assign: "WT (X :== a)" |
56 | Assign: "WT (X :== a)" |
60 |
57 |
61 Local: "WT c ==> |
58 | Local: "WT c ==> |
62 WT (LOCAL Y := a IN c)" |
59 WT (LOCAL Y := a IN c)" |
63 |
60 |
64 Semi: "[| WT c0; WT c1 |] ==> |
61 | Semi: "[| WT c0; WT c1 |] ==> |
65 WT (c0;; c1)" |
62 WT (c0;; c1)" |
66 |
63 |
67 If: "[| WT c0; WT c1 |] ==> |
64 | If: "[| WT c0; WT c1 |] ==> |
68 WT (IF b THEN c0 ELSE c1)" |
65 WT (IF b THEN c0 ELSE c1)" |
69 |
66 |
70 While: "WT c ==> |
67 | While: "WT c ==> |
71 WT (WHILE b DO c)" |
68 WT (WHILE b DO c)" |
72 |
69 |
73 Body: "body pn ~= None ==> |
70 | Body: "body pn ~= None ==> |
74 WT (BODY pn)" |
71 WT (BODY pn)" |
75 |
72 |
76 Call: "WT (BODY pn) ==> |
73 | Call: "WT (BODY pn) ==> |
77 WT (X:=CALL pn(a))" |
74 WT (X:=CALL pn(a))" |
78 |
75 |
79 inductive_cases WTs_elim_cases: |
76 inductive_cases WTs_elim_cases: |
80 "WT SKIP" "WT (X:==a)" "WT (LOCAL Y:=a IN c)" |
77 "WT SKIP" "WT (X:==a)" "WT (LOCAL Y:=a IN c)" |
81 "WT (c1;;c2)" "WT (IF b THEN c1 ELSE c2)" "WT (WHILE b DO c)" |
78 "WT (c1;;c2)" "WT (IF b THEN c1 ELSE c2)" "WT (WHILE b DO c)" |