Theory JinjaDCI.Objects

(*  Title:      JinjaDCI/Common/Objects.thy

    Author:     David von Oheimb, Susannah Mansky
    Copyright   1999 Technische Universitaet Muenchen, 2019-20 UIUC

    Based on the Jinja theory Common/Objects.thy by David von Oheimb
*)

section ‹ Objects and the Heap ›

theory Objects imports TypeRel Value begin

subsection‹ Objects ›

type_synonym
  fields = "vname × cname ⇀ val"  ― ‹field name, defining class, value›
type_synonym
  obj = "cname × fields"    ― ‹class instance with class name and fields›
type_synonym
  sfields = "vname ⇀ val"  ― ‹field name to value›

definition obj_ty  :: "obj ⇒ ty"
where
  "obj_ty obj  ≡  Class (fst obj)"

 ― ‹ initializes a given list of fields ›
definition init_fields :: "((vname × cname) × staticb × ty) list ⇒ fields"
where
  "init_fields FDTs  ≡  (map_of ∘ map (λ((F,D),b,T). ((F,D),default_val T))) FDTs"

definition init_sfields :: "((vname × cname) × staticb × ty) list ⇒ sfields"
where
  "init_sfields FDTs  ≡  (map_of ∘ map (λ((F,D),b,T). (F,default_val T))) FDTs"
  
  ― ‹a new, blank object with default values for instance fields:›
definition blank :: "'m prog ⇒ cname ⇒ obj"
where
  "blank P C ≡  (C,init_fields (ifields P C))"

  ― ‹a new, blank object with default values for static fields:›
definition sblank :: "'m prog ⇒ cname ⇒ sfields"
where
  "sblank P C ≡ init_sfields (isfields P C)"

lemma [simp]: "obj_ty (C,fs) = Class C"
(*<*)by (simp add: obj_ty_def)(*>*)

(* replaced all vname, cname in below with `char list' and ⇀ with returned option
  so that pretty printing works  -SM *)
translations
  (type) "fields" <= (type) "char list × char list ⇒ val option"
  (type) "obj" <= (type) "char list × fields"
  (type) "sfields" <= (type) "char list ⇒ val option"

subsection‹ Heap ›

type_synonym heap  = "addr ⇀ obj"

(* replaced addr with nat and ⇀ with returned option so that pretty printing works  -SM *)
translations
 (type) "heap" <= (type) "nat ⇒ obj option"

abbreviation
  cname_of :: "heap ⇒ addr ⇒ cname" where
  "cname_of hp a == fst (the (hp a))"

definition new_Addr  :: "heap ⇒ addr option"
where
  "new_Addr h  ≡  if ∃a. h a = None then Some(LEAST a. h a = None) else None"

definition cast_ok :: "'m prog ⇒ cname ⇒ heap ⇒ val ⇒ bool"
where
  "cast_ok P C h v  ≡  v = Null ∨ P ⊢ cname_of h (the_Addr v) ≼⇧* C"

definition hext :: "heap ⇒ heap ⇒ bool" (‹_ ⊴ _› [51,51] 50)
where
  "h ⊴ h'  ≡  ∀a C fs. h a = Some(C,fs) ⟶ (∃fs'. h' a = Some(C,fs'))"

primrec typeof_h :: "heap ⇒ val ⇒ ty option"  (‹typeof⇘_⇙›)
where
  "typeof⇘h⇙  Unit    = Some Void"
| "typeof⇘h⇙  Null    = Some NT"
| "typeof⇘h⇙ (Bool b) = Some Boolean"
| "typeof⇘h⇙ (Intg i) = Some Integer"
| "typeof⇘h⇙ (Addr a) = (case h a of None ⇒ None | Some(C,fs) ⇒ Some(Class C))"

lemma new_Addr_SomeD:
  "new_Addr h = Some a ⟹ h a = None"
 (*<*)by(fastforce simp: new_Addr_def split:if_splits intro:LeastI)(*>*)

lemma [simp]: "(typeof⇘h⇙ v = Some Boolean) = (∃b. v = Bool b)"
 (*<*)by(induct v) auto(*>*)

lemma [simp]: "(typeof⇘h⇙ v = Some Integer) = (∃i. v = Intg i)"
(*<*)by(cases v) auto(*>*)

lemma [simp]: "(typeof⇘h⇙ v = Some NT) = (v = Null)"
 (*<*)by(cases v) auto(*>*)

lemma [simp]: "(typeof⇘h⇙ v = Some(Class C)) = (∃a fs. v = Addr a ∧ h a = Some(C,fs))"
 (*<*)by(cases v) auto(*>*)

lemma [simp]: "h a = Some(C,fs) ⟹ typeof⇘(h(a↦(C,fs')))⇙ v = typeof⇘h⇙ v"
 (*<*)by(induct v) (auto simp:fun_upd_apply)(*>*)

text‹ For literal values the first parameter of @{term typeof} can be
set to @{term empty} because they do not contain addresses: ›

abbreviation
  typeof :: "val ⇒ ty option" where
  "typeof v == typeof_h Map.empty v"

lemma typeof_lit_typeof:
  "typeof v = Some T ⟹ typeof⇘h⇙ v = Some T"
 (*<*)by(cases v) auto(*>*)

lemma typeof_lit_is_type: 
  "typeof v = Some T ⟹ is_type P T"
 (*<*)by (induct v) (auto simp:is_type_def)(*>*)


subsection ‹ Heap extension @{text"⊴"} ›

lemma hextI: "∀a C fs. h a = Some(C,fs) ⟶ (∃fs'. h' a = Some(C,fs')) ⟹ h ⊴ h'"
(*<*)by(auto simp: hext_def)(*>*)

lemma hext_objD: "⟦ h ⊴ h'; h a = Some(C,fs) ⟧ ⟹ ∃fs'. h' a = Some(C,fs')"
(*<*)by(auto simp: hext_def)(*>*)

lemma hext_refl [iff]: "h ⊴ h"
(*<*)by (rule hextI) fast(*>*)

lemma hext_new [simp]: "h a = None ⟹ h ⊴ h(a↦x)"
(*<*)by (rule hextI) (auto simp:fun_upd_apply)(*>*)

lemma hext_trans: "⟦ h ⊴ h'; h' ⊴ h'' ⟧ ⟹ h ⊴ h''"
(*<*)by (rule hextI) (fast dest: hext_objD)(*>*)

lemma hext_upd_obj: "h a = Some (C,fs) ⟹ h ⊴ h(a↦(C,fs'))"
(*<*)by (rule hextI) (auto simp:fun_upd_apply)(*>*)

lemma hext_typeof_mono: "⟦ h ⊴ h'; typeof⇘h⇙ v = Some T ⟧ ⟹ typeof⇘h'⇙ v = Some T"
(*<*)
proof(cases v)
  case Addr assume "h ⊴ h'" and "typeof⇘h⇙ v = ⌊T⌋"
  then show ?thesis using Addr by(fastforce simp:hext_def)
qed simp_all
(*>*)

subsection‹ Static field information function ›

datatype init_state = Done | Processing | Prepared | Error
	― ‹@{term Done} = initialized›
	― ‹@{term Processing} = currently being initialized›
	― ‹@{term Prepared} = uninitialized and not currently being initialized›
	― ‹@{term Error} = previous initialization attempt resulted in erroneous state›

inductive iprog :: "init_state ⇒ init_state ⇒ bool" (‹_ ≤⇩i _› [51,51] 50)
where
  [simp]: "Prepared ≤⇩i i"
| [simp]: "Processing ≤⇩i Done"
| [simp]: "Processing ≤⇩i Error"
| [simp]: "i ≤⇩i i"

lemma iprog_Done[simp]: "(Done ≤⇩i i) = (i = Done)"
 by(simp only: iprog.simps, simp)

lemma iprog_Error[simp]: "(Error ≤⇩i i) = (i = Error)"
 by(simp only: iprog.simps, simp)

lemma iprog_Processing[simp]: "(Processing ≤⇩i i) = (i = Done ∨ i = Error ∨ i = Processing)"
 by(simp only: iprog.simps, simp)

lemma iprog_trans: "⟦ i ≤⇩i i'; i' ≤⇩i i'' ⟧ ⟹ i ≤⇩i i''"
(*<*)by(case_tac i; case_tac i') simp_all(*>*)

subsection‹ Static Heap ›

text ‹The static heap (sheap) is used for storing information about static
 field values and initialization status for classes.›

type_synonym
  sheap = "cname ⇀ sfields × init_state"

translations
 (type) "sheap" <= (type) "char list ⇒ (sfields × init_state) option"

definition shext :: "sheap ⇒ sheap ⇒ bool" (‹_ ⊴⇩s _› [51,51] 50)
where
  "sh ⊴⇩s sh'  ≡  ∀C sfs i. sh C = Some(sfs,i) ⟶ (∃sfs' i'. sh' C = Some(sfs',i') ∧ i ≤⇩i i')"


lemma shextI: "∀C sfs i. sh C = Some(sfs,i) ⟶ (∃sfs' i'. sh' C = Some(sfs',i') ∧ i ≤⇩i i') ⟹ sh ⊴⇩s sh'"
(*<*)by(auto simp: shext_def)(*>*)

lemma shext_objD: "⟦ sh ⊴⇩s sh'; sh C = Some(sfs,i) ⟧ ⟹ ∃sfs' i'. sh' C = Some(sfs', i') ∧ i ≤⇩i i'"
(*<*)by(auto simp: shext_def)(*>*)

lemma shext_refl [iff]: "sh ⊴⇩s sh"
(*<*)by (rule shextI) auto(*>*)

lemma shext_new [simp]: "sh C = None ⟹ sh ⊴⇩s sh(C↦x)"
(*<*)by (rule shextI) (auto simp:fun_upd_apply)(*>*)

lemma shext_trans: "⟦ sh ⊴⇩s sh'; sh' ⊴⇩s sh'' ⟧ ⟹ sh ⊴⇩s sh''"
(*<*)by (rule shextI) (fast dest: iprog_trans shext_objD)(*>*)

lemma shext_upd_obj: "⟦ sh C = Some (sfs,i); i ≤⇩i i' ⟧ ⟹ sh ⊴⇩s sh(C↦(sfs',i'))"
(*<*)by (rule shextI) (auto simp:fun_upd_apply)(*>*)

end