|
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) | |
|
25 Semi exp exp ("_;/ _" [61,60] 60) | |
|
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)" | |
|
59 Semi: |
|
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 |