43158
|
1 |
theory OO imports Main begin
|
|
2 |
|
|
3 |
subsection "Towards an OO Language: A Language of Records"
|
|
4 |
|
|
5 |
(* FIXME: move to HOL/Fun *)
|
|
6 |
abbreviation fun_upd2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c"
|
|
7 |
("_/'((2_,_ :=/ _)')" [1000,0,0,0] 900)
|
|
8 |
where "f(x,y := z) == f(x := (f x)(y := z))"
|
|
9 |
|
|
10 |
type_synonym addr = nat
|
|
11 |
datatype ref = null | Ref addr
|
|
12 |
|
|
13 |
type_synonym obj = "string \<Rightarrow> ref"
|
|
14 |
type_synonym venv = "string \<Rightarrow> ref"
|
|
15 |
type_synonym store = "addr \<Rightarrow> obj"
|
|
16 |
|
|
17 |
datatype exp =
|
|
18 |
Null |
|
|
19 |
New |
|
|
20 |
V string |
|
|
21 |
Faccess exp string ("_\<bullet>/_" [63,1000] 63) |
|
|
22 |
Vassign string exp ("(_ ::=/ _)" [1000,61] 62) |
|
|
23 |
Fassign exp string exp ("(_\<bullet>_ ::=/ _)" [63,0,62] 62) |
|
|
24 |
Mcall exp string exp ("(_\<bullet>/_<_>)" [63,0,0] 63) |
|
47818
|
25 |
Seq exp exp ("_;/ _" [61,60] 60) |
|
43158
|
26 |
If bexp exp exp ("IF _/ THEN (2_)/ ELSE (2_)" [0,0,61] 61)
|
|
27 |
and bexp = B bool | Not bexp | And bexp bexp | Eq exp exp
|
|
28 |
|
|
29 |
type_synonym menv = "string \<Rightarrow> exp"
|
|
30 |
type_synonym config = "venv \<times> store \<times> addr"
|
|
31 |
|
|
32 |
inductive
|
|
33 |
big_step :: "menv \<Rightarrow> exp \<times> config \<Rightarrow> ref \<times> config \<Rightarrow> bool"
|
|
34 |
("(_ \<turnstile>/ (_/ \<Rightarrow> _))" [60,0,60] 55) and
|
|
35 |
bval :: "menv \<Rightarrow> bexp \<times> config \<Rightarrow> bool \<times> config \<Rightarrow> bool"
|
|
36 |
("_ \<turnstile> _ \<rightarrow> _" [60,0,60] 55)
|
|
37 |
where
|
|
38 |
Null:
|
|
39 |
"me \<turnstile> (Null,c) \<Rightarrow> (null,c)" |
|
|
40 |
New:
|
|
41 |
"me \<turnstile> (New,ve,s,n) \<Rightarrow> (Ref n,ve,s(n := (\<lambda>f. null)),n+1)" |
|
|
42 |
Vaccess:
|
|
43 |
"me \<turnstile> (V x,ve,sn) \<Rightarrow> (ve x,ve,sn)" |
|
|
44 |
Faccess:
|
|
45 |
"me \<turnstile> (e,c) \<Rightarrow> (Ref a,ve',s',n') \<Longrightarrow>
|
|
46 |
me \<turnstile> (e\<bullet>f,c) \<Rightarrow> (s' a f,ve',s',n')" |
|
|
47 |
Vassign:
|
|
48 |
"me \<turnstile> (e,c) \<Rightarrow> (r,ve',sn') \<Longrightarrow>
|
|
49 |
me \<turnstile> (x ::= e,c) \<Rightarrow> (r,ve'(x:=r),sn')" |
|
|
50 |
Fassign:
|
|
51 |
"\<lbrakk> me \<turnstile> (oe,c\<^isub>1) \<Rightarrow> (Ref a,c\<^isub>2); me \<turnstile> (e,c\<^isub>2) \<Rightarrow> (r,ve\<^isub>3,s\<^isub>3,n\<^isub>3) \<rbrakk> \<Longrightarrow>
|
|
52 |
me \<turnstile> (oe\<bullet>f ::= e,c\<^isub>1) \<Rightarrow> (r,ve\<^isub>3,s\<^isub>3(a,f := r),n\<^isub>3)" |
|
|
53 |
Mcall:
|
|
54 |
"\<lbrakk> me \<turnstile> (oe,c\<^isub>1) \<Rightarrow> (or,c\<^isub>2); me \<turnstile> (pe,c\<^isub>2) \<Rightarrow> (pr,ve\<^isub>3,sn\<^isub>3);
|
|
55 |
ve = (\<lambda>x. null)(''this'' := or, ''param'' := pr);
|
|
56 |
me \<turnstile> (me m,ve,sn\<^isub>3) \<Rightarrow> (r,ve',sn\<^isub>4) \<rbrakk>
|
|
57 |
\<Longrightarrow>
|
|
58 |
me \<turnstile> (oe\<bullet>m<pe>,c\<^isub>1) \<Rightarrow> (r,ve\<^isub>3,sn\<^isub>4)" |
|
47818
|
59 |
Seq:
|
43158
|
60 |
"\<lbrakk> me \<turnstile> (e\<^isub>1,c\<^isub>1) \<Rightarrow> (r,c\<^isub>2); me \<turnstile> (e\<^isub>2,c\<^isub>2) \<Rightarrow> c\<^isub>3 \<rbrakk> \<Longrightarrow>
|
|
61 |
me \<turnstile> (e\<^isub>1; e\<^isub>2,c\<^isub>1) \<Rightarrow> c\<^isub>3" |
|
|
62 |
IfTrue:
|
|
63 |
"\<lbrakk> me \<turnstile> (b,c\<^isub>1) \<rightarrow> (True,c\<^isub>2); me \<turnstile> (e\<^isub>1,c\<^isub>2) \<Rightarrow> c\<^isub>3 \<rbrakk> \<Longrightarrow>
|
|
64 |
me \<turnstile> (IF b THEN e\<^isub>1 ELSE e\<^isub>2,c\<^isub>1) \<Rightarrow> c\<^isub>3" |
|
|
65 |
IfFalse:
|
|
66 |
"\<lbrakk> me \<turnstile> (b,c\<^isub>1) \<rightarrow> (False,c\<^isub>2); me \<turnstile> (e\<^isub>2,c\<^isub>2) \<Rightarrow> c\<^isub>3 \<rbrakk> \<Longrightarrow>
|
|
67 |
me \<turnstile> (IF b THEN e\<^isub>1 ELSE e\<^isub>2,c\<^isub>1) \<Rightarrow> c\<^isub>3" |
|
|
68 |
|
|
69 |
"me \<turnstile> (B bv,c) \<rightarrow> (bv,c)" |
|
|
70 |
|
|
71 |
"me \<turnstile> (b,c\<^isub>1) \<rightarrow> (bv,c\<^isub>2) \<Longrightarrow> me \<turnstile> (Not b,c\<^isub>1) \<rightarrow> (\<not>bv,c\<^isub>2)" |
|
|
72 |
|
|
73 |
"\<lbrakk> me \<turnstile> (b\<^isub>1,c\<^isub>1) \<rightarrow> (bv\<^isub>1,c\<^isub>2); me \<turnstile> (b\<^isub>2,c\<^isub>2) \<rightarrow> (bv\<^isub>2,c\<^isub>3) \<rbrakk> \<Longrightarrow>
|
|
74 |
me \<turnstile> (And b\<^isub>1 b\<^isub>2,c\<^isub>1) \<rightarrow> (bv\<^isub>1\<and>bv\<^isub>2,c\<^isub>3)" |
|
|
75 |
|
|
76 |
"\<lbrakk> me \<turnstile> (e\<^isub>1,c\<^isub>1) \<Rightarrow> (r\<^isub>1,c\<^isub>2); me \<turnstile> (e\<^isub>2,c\<^isub>2) \<Rightarrow> (r\<^isub>2,c\<^isub>3) \<rbrakk> \<Longrightarrow>
|
|
77 |
me \<turnstile> (Eq e\<^isub>1 e\<^isub>2,c\<^isub>1) \<rightarrow> (r\<^isub>1=r\<^isub>2,c\<^isub>3)"
|
|
78 |
|
|
79 |
|
|
80 |
code_pred (modes: i => i => o => bool) big_step .
|
|
81 |
|
|
82 |
text{* Example: natural numbers encoded as objects with a predecessor
|
|
83 |
field. Null is zero. Method succ adds an object in front, method add
|
|
84 |
adds as many objects in front as the parameter specifies.
|
|
85 |
|
|
86 |
First, the method bodies: *}
|
|
87 |
|
|
88 |
definition
|
|
89 |
"m_succ = (''s'' ::= New)\<bullet>''pred'' ::= V ''this''; V ''s''"
|
|
90 |
|
|
91 |
definition "m_add =
|
|
92 |
IF Eq (V ''param'') Null
|
|
93 |
THEN V ''this''
|
|
94 |
ELSE V ''this''\<bullet>''succ''<Null>\<bullet>''add''<V ''param''\<bullet>''pred''>"
|
|
95 |
|
|
96 |
text{* The method environment: *}
|
|
97 |
definition
|
|
98 |
"menv = (\<lambda>m. Null)(''succ'' := m_succ, ''add'' := m_add)"
|
|
99 |
|
|
100 |
text{* The main code, adding 1 and 2: *}
|
|
101 |
definition "main =
|
|
102 |
''1'' ::= Null\<bullet>''succ''<Null>;
|
|
103 |
''2'' ::= V ''1''\<bullet>''succ''<Null>;
|
|
104 |
V ''2'' \<bullet> ''add'' <V ''1''>"
|
|
105 |
|
|
106 |
text{* Execution of semantics. The final variable environment and store are
|
|
107 |
converted into lists of references based on given lists of variable and field
|
|
108 |
names to extract. *}
|
|
109 |
|
|
110 |
values
|
|
111 |
"{(r, map ve' [''1'',''2''], map (\<lambda>n. map (s' n)[''pred'']) [0..<n])|
|
|
112 |
r ve' s' n. menv \<turnstile> (main, \<lambda>x. null, nth[], 0) \<Rightarrow> (r,ve',s',n)}"
|
|
113 |
|
|
114 |
end
|