Quelle OO.thy Sprache: 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"
  (\<open>_/'((2_,_ :=/ _)')\<close> [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       (\<open>_\<bullet>/_\<close> [63,1000] 63) |
  Vassign string exp       (\<open>(_ ::=/ _)\<close> [1000,61] 62) |
  Fassign exp string exp   (\<open>(_\<bullet>_ ::=/ _)\<close> [63,0,62] 62) |
  Mcall exp string exp     (\<open>(_\<bullet>/_<_>)\<close> [63,0,0] 63) |
  Seq exp exp              (\<open>_;/ _\<close> [61,60] 60) |
  If bexp exp exp          (\<open>IF _/ THEN (2_)/ ELSE (2_)\<close> [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"
    (\<open>(_ \<turnstile>/ (_/ \<Rightarrow> _))\<close> [60,0,60] 55) and
  bval ::  "menv \ bexp \ config \ bool \ config \ bool"
    (\<open>_ \<turnstile> _ \<rightarrow> _\<close> [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)" for or |
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

quality100%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.