theory OO imports Util begin subsection "Towards an OO Language: A Language of Records" (* FIXME: move to HOL/Fun *) abbreviation fun_upd2 :: "('a \ 'b \ 'c) \ 'a \ 'b \ 'c \ 'a \ 'b \ 'c" ("_/'((2_,_ :=/ _)')" [1000,0,0,0] 900) where "f(x,y := z) == f(x := (f x)(y := z))" types addr = nat datatype ref = null | Ref addr types obj = "string \ ref" venv = "string \ ref" store = "addr \ obj" datatype exp = Null | New | V string | Faccess exp string ("_\/_" [63,1000] 63) | Vassign string exp ("(_ ::=/ _)" [1000,61] 62) | Fassign exp string exp ("(_\_ ::=/ _)" [63,0,62] 62) | Mcall exp string exp ("(_\/_<_>)" [63,0,0] 63) | Semi exp exp ("_;/ _" [61,60] 60) | If bexp exp exp ("IF _/ THEN (2_)/ ELSE (2_)" [0,0,61] 61) and bexp = B bool | Not bexp | And bexp bexp | Eq exp exp types menv = "string \ exp" config = "venv \ store \ addr" inductive big_step :: "menv \ exp \ config \ ref \ config \ bool" ("(_ \/ (_/ \ _))" [60,0,60] 55) and bval :: "menv \ bexp \ config \ bool \ config \ bool" ("_ \ _ \ _" [60,0,60] 55) where Null: "me \ (Null,c) \ (null,c)" | New: "me \ (New,ve,s,n) \ (Ref n,ve,s(n := (\f. null)),n+1)" | Vaccess: "me \ (V x,ve,sn) \ (ve x,ve,sn)" | Faccess: "me \ (e,c) \ (Ref a,ve',s',n') \ me \ (e\f,c) \ (s' a f,ve',s',n')" | Vassign: "me \ (e,c) \ (r,ve',sn') \ me \ (x ::= e,c) \ (r,ve'(x:=r),sn')" | Fassign: "\ me \ (oe,c\<^isub>1) \ (Ref a,c\<^isub>2); me \ (e,c\<^isub>2) \ (r,ve\<^isub>3,s\<^isub>3,n\<^isub>3) \ \ me \ (oe\f ::= e,c\<^isub>1) \ (r,ve\<^isub>3,s\<^isub>3(a,f := r),n\<^isub>3)" | Mcall: "\ me \ (oe,c\<^isub>1) \ (or,c\<^isub>2); me \ (pe,c\<^isub>2) \ (pr,ve\<^isub>3,sn\<^isub>3); ve = (\x. null)(''this'' := or, ''param'' := pr); me \ (me m,ve,sn\<^isub>3) \ (r,ve',sn\<^isub>4) \ \ me \ (oe\m,c\<^isub>1) \ (r,ve\<^isub>3,sn\<^isub>4)" | Semi: "\ me \ (e\<^isub>1,c\<^isub>1) \ (r,c\<^isub>2); me \ (e\<^isub>2,c\<^isub>2) \ c\<^isub>3 \ \ me \ (e\<^isub>1; e\<^isub>2,c\<^isub>1) \ c\<^isub>3" | IfTrue: "\ me \ (b,c\<^isub>1) \ (True,c\<^isub>2); me \ (e\<^isub>1,c\<^isub>2) \ c\<^isub>3 \ \ me \ (IF b THEN e\<^isub>1 ELSE e\<^isub>2,c\<^isub>1) \ c\<^isub>3" | IfFalse: "\ me \ (b,c\<^isub>1) \ (False,c\<^isub>2); me \ (e\<^isub>2,c\<^isub>2) \ c\<^isub>3 \ \ me \ (IF b THEN e\<^isub>1 ELSE e\<^isub>2,c\<^isub>1) \ c\<^isub>3" | "me \ (B bv,c) \ (bv,c)" | "me \ (b,c\<^isub>1) \ (bv,c\<^isub>2) \ me \ (Not b,c\<^isub>1) \ (\bv,c\<^isub>2)" | "\ me \ (b\<^isub>1,c\<^isub>1) \ (bv\<^isub>1,c\<^isub>2); me \ (b\<^isub>2,c\<^isub>2) \ (bv\<^isub>2,c\<^isub>3) \ \ me \ (And b\<^isub>1 b\<^isub>2,c\<^isub>1) \ (bv\<^isub>1\bv\<^isub>2,c\<^isub>3)" | "\ me \ (e\<^isub>1,c\<^isub>1) \ (r\<^isub>1,c\<^isub>2); me \ (e\<^isub>2,c\<^isub>2) \ (r\<^isub>2,c\<^isub>3) \ \ me \ (Eq e\<^isub>1 e\<^isub>2,c\<^isub>1) \ (r\<^isub>1=r\<^isub>2,c\<^isub>3)" code_pred (modes: i => i => o => bool) big_step . text{* Execution of semantics. The final variable environment and store are converted into lists of references based on given lists of variable and field names to extract. *} inductive exec :: "menv \ exp \ string list \ string list \ ref \ ref list \ ref list list \ bool" where "me \ (e,(\x. null),nth[],0) \ (r,ve',s',n) \ exec me e xs fs r (map ve' xs) (map (\n. map (s' n) fs) [0..''pred'' ::= V ''this''; V ''s''" definition "m_add = IF Eq (V ''param'') Null THEN V ''this'' ELSE V ''this''\''succ''\''add''''pred''>" text{* The method environment: *} definition "menv = (\m. Null)(''succ'' := m_succ, ''add'' := m_add)" text{* The main code, adding 1 and 2: *} definition "main = ''1'' ::= Null\''succ''; ''2'' ::= V ''1''\''succ''; V ''2'' \ ''add'' " values "{(r,vl,ol). exec menv main [''1'',''2''] [''pred''] r vl ol}" end