Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/HOL/NanoJava/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 6 kB

Quelle State.thy Sprache: Isabelle

(*  Title:      HOL/NanoJava/State.thy
    Author:     David von Oheimb
    Copyright   2001 Technische Universitaet Muenchen
*)

section "Program State"

theory State imports TypeRel begin

definition body :: "cname \ mname => stmt" where
"body \ \(C,m). bdy (the (method C m))"

text \<open>Locations, i.e.\ abstract references to objects\<close>
typedecl loc

datatype val
  = Null        \<comment> \<open>null reference\<close>
  | Addr loc    \<comment> \<open>address, i.e. location of object\<close>

type_synonym fields
        = "(fname \ val)"

type_synonym
        obj = "cname \ fields"

translations
  (type) "fields" \<leftharpoondown> (type) "fname => val option"
  (type) "obj"    \<leftharpoondown> (type) "cname \<times> fields"

definition init_vars :: "('a \ 'b) => ('a \ val)" where
"init_vars m == map_option (\T. Null) o m"

text \<open>private:\<close>
type_synonym heap = "loc \ obj"
type_synonym locals = "vname \ val"

text \<open>private:\<close>
record  state
        = heap   :: heap
          locals :: locals

translations
  (type) "heap" \<leftharpoondown> (type) "loc => obj option"
  (type) "locals" \<leftharpoondown> (type) "vname => val option"
  (type) "state" \<leftharpoondown> (type) "(|heap :: heap, locals :: locals|)"

definition del_locs :: "state => state" where
"del_locs s \ s (| locals := Map.empty |)"

definition init_locs     :: "cname => mname => state => state" where
"init_locs C m s \ s (| locals := locals s ++
                         init_vars (map_of (lcl (the (method C m)))) |)"

text \<open>The first parameter of \<^term>\<open>set_locs\<close> is of type \<^typ>\<open>state\<close>
        rather than \<^typ>\<open>locals\<close> in order to keep \<^typ>\<open>locals\<close> private.\<close>
definition set_locs :: "state => state => state" where
"set_locs s s' \ s' (| locals := locals s |)"

definition get_local     :: "state => vname => val" (\<open>_<_>\<close> [99,0] 99) where
"get_local s x \ the (locals s x)"

\<comment> \<open>local function:\<close>
definition get_obj       :: "state => loc => obj" where
"get_obj s a \ the (heap s a)"

definition obj_class     :: "state => loc => cname" where
"obj_class s a \ fst (get_obj s a)"

definition get_field     :: "state => loc => fname => val" where
"get_field s a f \ the (snd (get_obj s a) f)"

\<comment> \<open>local function:\<close>
definition hupd       :: "loc => obj => state => state"   (\<open>hupd'(_\<mapsto>_')\<close> [10,10] 1000) where
"hupd a obj s \ s (| heap := ((heap s)(a\obj))|)"

definition lupd       :: "vname => val => state => state" (\<open>lupd'(_\<mapsto>_')\<close> [10,10] 1000) where
"lupd x v s \ s (| locals := ((locals s)(x\v ))|)"

definition new_obj :: "loc => cname => state => state" where
"new_obj a C \ hupd(a\(C,init_vars (field C)))"

definition upd_obj    :: "loc => fname => val => state => state" where
"upd_obj a f v s \ let (C,fs) = the (heap s a) in hupd(a\(C,fs(f\v))) s"

definition new_Addr      :: "state => val" where
"new_Addr s == SOME v. (\a. v = Addr a \ (heap s) a = None) | v = Null"

subsection "Properties not used in the meta theory"

lemma locals_upd_id [simp]: "s\locals := locals s\ = s"
by simp

lemma lupd_get_local_same [simp]: "lupd(x\v) s = v"
by (simp add: lupd_def get_local_def)

lemma lupd_get_local_other [simp]: "x \ y \ lupd(x\v) s = s"
apply (drule not_sym)
by (simp add: lupd_def get_local_def)

lemma get_field_lupd [simp]:
  "get_field (lupd(x\y) s) a f = get_field s a f"
by (simp add: lupd_def get_field_def get_obj_def)

lemma get_field_set_locs [simp]:
  "get_field (set_locs l s) a f = get_field s a f"
by (simp add: lupd_def get_field_def set_locs_def get_obj_def)

lemma get_field_del_locs [simp]:
  "get_field (del_locs s) a f = get_field s a f"
by (simp add: lupd_def get_field_def del_locs_def get_obj_def)

lemma new_obj_get_local [simp]: "new_obj a C s = s"
by (simp add: new_obj_def hupd_def get_local_def)

lemma heap_lupd [simp]: "heap (lupd(x\y) s) = heap s"
by (simp add: lupd_def)

lemma heap_hupd_same [simp]: "heap (hupd(a\obj) s) a = Some obj"
by (simp add: hupd_def)

lemma heap_hupd_other [simp]: "aa \ a \ heap (hupd(aa\obj) s) a = heap s a"
apply (drule not_sym)
by (simp add: hupd_def)

lemma hupd_hupd [simp]: "hupd(a\obj) (hupd(a\obj') s) = hupd(a\obj) s"
by (simp add: hupd_def)

lemma heap_del_locs [simp]: "heap (del_locs s) = heap s"
by (simp add: del_locs_def)

lemma heap_set_locs [simp]: "heap (set_locs l s) = heap s"
by (simp add: set_locs_def)

lemma hupd_lupd [simp]:
  "hupd(a\obj) (lupd(x\y) s) = lupd(x\y) (hupd(a\obj) s)"
by (simp add: hupd_def lupd_def)

lemma hupd_del_locs [simp]:
  "hupd(a\obj) (del_locs s) = del_locs (hupd(a\obj) s)"
by (simp add: hupd_def del_locs_def)

lemma new_obj_lupd [simp]:
  "new_obj a C (lupd(x\y) s) = lupd(x\y) (new_obj a C s)"
by (simp add: new_obj_def)

lemma new_obj_del_locs [simp]:
  "new_obj a C (del_locs s) = del_locs (new_obj a C s)"
by (simp add: new_obj_def)

lemma upd_obj_lupd [simp]:
  "upd_obj a f v (lupd(x\y) s) = lupd(x\y) (upd_obj a f v s)"
by (simp add: upd_obj_def Let_def split_beta)

lemma upd_obj_del_locs [simp]:
  "upd_obj a f v (del_locs s) = del_locs (upd_obj a f v s)"
by (simp add: upd_obj_def Let_def split_beta)

lemma get_field_hupd_same [simp]:
"get_field (hupd(a\(C, fs)) s) a = the \ fs"
apply (rule ext)
by (simp add: get_field_def get_obj_def)

lemma get_field_hupd_other [simp]:
"aa \ a \ get_field (hupd(aa\obj) s) a = get_field s a"
apply (rule ext)
by (simp add: get_field_def get_obj_def)

lemma new_AddrD:
"new_Addr s = v \ (\a. v = Addr a \ heap s a = None) | v = Null"
apply (unfold new_Addr_def)
apply (erule subst)
apply (rule someI)
apply (rule disjI2)
apply (rule HOL.refl)
done

end

quality100%

¤ Dauer der Verarbeitung: 0.1 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.