Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: OO.thy Sprache: Isabelle

Original von: Isabelle^©

theory OO imports Main 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))"

type_synonym addr = nat
datatype ref = null | Ref addr

type_synonym obj = "string \ ref"
type_synonym venv = "string \ ref"
type_synonym 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) |
  Seq 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

type_synonym menv = "string \ exp"
type_synonym 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 \<turnstile> (e\<bullet>f,c) \<Rightarrow> (s' a f,ve',s',n')" |
Vassign:
"me \ (e,c) \ (r,ve',sn') \
me \<turnstile> (x ::= e,c) \<Rightarrow> (r,ve'(x:=r),sn')" |
Fassign:
"\ me \ (oe,c\<^sub>1) \ (Ref a,c\<^sub>2); me \ (e,c\<^sub>2) \ (r,ve\<^sub>3,s\<^sub>3,n\<^sub>3) \ \
me \<turnstile> (oe\<bullet>f ::= e,c\<^sub>1) \<Rightarrow> (r,ve\<^sub>3,s\<^sub>3(a,f := r),n\<^sub>3)" |
Mcall:
"\ me \ (oe,c\<^sub>1) \ (or,c\<^sub>2); me \ (pe,c\<^sub>2) \ (pr,ve\<^sub>3,sn\<^sub>3);
   ve = (\<lambda>x. null)(''this'' := or, ''param'' := pr);
   me \<turnstile> (me m,ve,sn\<^sub>3) \<Rightarrow> (r,ve',sn\<^sub>4) \<rbrakk>
  \<Longrightarrow>
me \<turnstile> (oe\<bullet>m<pe>,c\<^sub>1) \<Rightarrow> (r,ve\<^sub>3,sn\<^sub>4)" |
Seq:
"\ me \ (e\<^sub>1,c\<^sub>1) \ (r,c\<^sub>2); me \ (e\<^sub>2,c\<^sub>2) \ c\<^sub>3 \ \
me \<turnstile> (e\<^sub>1; e\<^sub>2,c\<^sub>1) \<Rightarrow> c\<^sub>3" |
IfTrue:
"\ me \ (b,c\<^sub>1) \ (True,c\<^sub>2); me \ (e\<^sub>1,c\<^sub>2) \ c\<^sub>3 \ \
me \<turnstile> (IF b THEN e\<^sub>1 ELSE e\<^sub>2,c\<^sub>1) \<Rightarrow> c\<^sub>3" |
IfFalse:
"\ me \ (b,c\<^sub>1) \ (False,c\<^sub>2); me \ (e\<^sub>2,c\<^sub>2) \ c\<^sub>3 \ \
me \<turnstile> (IF b THEN e\<^sub>1 ELSE e\<^sub>2,c\<^sub>1) \<Rightarrow> c\<^sub>3" |

"me \ (B bv,c) \ (bv,c)" |

"me \ (b,c\<^sub>1) \ (bv,c\<^sub>2) \ me \ (Not b,c\<^sub>1) \ (\bv,c\<^sub>2)" |

"\ me \ (b\<^sub>1,c\<^sub>1) \ (bv\<^sub>1,c\<^sub>2); me \ (b\<^sub>2,c\<^sub>2) \ (bv\<^sub>2,c\<^sub>3) \ \
me \<turnstile> (And b\<^sub>1 b\<^sub>2,c\<^sub>1) \<rightarrow> (bv\<^sub>1\<and>bv\<^sub>2,c\<^sub>3)" |

"\ me \ (e\<^sub>1,c\<^sub>1) \ (r\<^sub>1,c\<^sub>2); me \ (e\<^sub>2,c\<^sub>2) \ (r\<^sub>2,c\<^sub>3) \ \
me \<turnstile> (Eq e\<^sub>1 e\<^sub>2,c\<^sub>1) \<rightarrow> (r\<^sub>1=r\<^sub>2,c\<^sub>3)"

code_pred (modes: i => i => o => bool) big_step .

text\<open>Example: natural numbers encoded as objects with a predecessor
field. Null is zero. Method succ adds an object in front, method add
adds as many objects in front as the parameter specifies.

First, the method bodies:\<close>

definition
"m_succ = (''s'' ::= New)\''pred'' ::= V ''this''; V ''s''"

definition "m_add =
  IF Eq (V ''param'') Null
  THEN V ''this''
  ELSE V ''this''\<bullet>''succ''<Null>\<bullet>''add''<V ''param''\<bullet>''pred''>"

text\<open>The method environment:\<close>
definition
"menv = (\m. Null)(''succ'' := m_succ, ''add'' := m_add)"

text\<open>The main code, adding 1 and 2:\<close>
definition "main =
  ''1'' ::= Null\<bullet>''succ''<Null>;
  ''2'' ::= V ''1''\<bullet>''succ''<Null>;
  V ''2'' \<bullet> ''add'' <V ''1''>"

text\<open>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.\<close>

values
"{(r, map ve' [''1'',''2''], map (\n. map (s' n)[''pred'']) [0..
    r ve' s' n. menv \<turnstile> (main, \<lambda>x. null, nth[], 0) \<Rightarrow> (r,ve',s',n)}"

end

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.