| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/REXX/ (Beweissystem der NASA Version 6.0.9©) Datei vom 2.3.2012 mit Größe 1 kB |
|
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 \ (\<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 \ type_synonym venv = "string \ type_synonym store = "addr \ 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 \ type_synonym config = "venv \ inductive big_step :: "menv \ (\<open>(_ \<turnstile>/ (_/ \<Rightarrow> _))\<close> [60,0,60] 55) and bval :: "menv \ (\<open>_ \<turnstile> _ \<rightarrow> _\<close> [60,0,60] 55) where Null: "me \ New: "me \ Vaccess: "me \ Faccess: "me \ me \<turnstile> (e\<bullet>f,c) \<Rightarrow> (s' a f,ve',s',n')" | Vassign: "me \ me \<turnstile> (x ::= e,c) \<Rightarrow> (r,ve'(x:=r),sn')" | Fassign: "\ me \<turnstile> (oe\<bullet>f ::= e,c\<^sub>1) \<Rightarrow> (r,ve\<^sub>3,s\<^sub>3(a,f := r),n\<^su Mcall: "\ 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 \<turnstile> (e\<^sub>1; e\<^sub>2,c\<^sub>1) \<Rightarrow> c\<^sub>3" | IfTrue: "\ me \<turnstile> (IF b THEN e\<^sub>1 ELSE e\<^sub>2,c\<^sub>1) \<Rightarrow> c\<^sub>3" | IfFalse: "\ me \<turnstile> (IF b THEN e\<^sub>1 ELSE e\<^sub>2,c\<^sub>1) \<Rightarrow> c\<^sub>3" | "me \ "me \ "\ me \<turnstile> (And b\<^sub>1 b\<^sub>2,c\<^sub>1) \<rightarrow> (bv\<^sub>1\<and>bv\<^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)\ 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 = (\ 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 (\ r ve' s' n. menv \<turnstile> (main, \<lambda>x. null, nth[], 0) \<Rightarrow> (r,ve',s',n)}" end ¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28