Theory Location

(*  Title:       Jive Data and Store Model
    Author:      Norbert Schirmer <schirmer at informatik.tu-muenchen.de>, 2003
    Maintainer:  Nicole Rauch <rauch at informatik.uni-kl.de>
    License:     LGPL
*)

section ‹Location›

theory Location
imports AttributesIndep "../Isabelle/Value"
begin 

text ‹A storage location can be a field of an object, a static field,
 the length of an array, or the contents of an array.  
›

datatype Location = objLoc    CAttId ObjectId     ― ‹field in object› 
                  | staticLoc AttId               ― ‹static field in concrete class›
                  | arrLenLoc Arraytype ObjectId   ― ‹length of an array›
                  | arrLoc    Arraytype ObjectId nat ― ‹contents of an array›

text ‹We only directly support one-dimensional arrays. Multidimensional
arrays can be simulated by arrays of references to arrays.
›

text ‹The function ‹ltype› yields the content type of a location.›
definition ltype:: "Location ⇒ Javatype" where
"ltype l = (case l of
              objLoc cf a  ⇒ rtype (att cf)
            | staticLoc f     ⇒ rtype f
            | arrLenLoc T a   ⇒ IntgT
            | arrLoc T a i ⇒ at2jt T)" 

lemma ltype_simps [simp]:
"ltype (objLoc cf a)  = rtype (att cf)"
"ltype (staticLoc f)     = rtype f"
"ltype (arrLenLoc T a)   = IntgT"
"ltype (arrLoc T a i) = at2jt T" 
  by (simp_all add: ltype_def)

text ‹Discriminator functions to test whether a location denotes an array length
or whether it denotes a static object. Currently, the discriminator functions for
object and array locations are not specified. They can be added if they are needed.
›

definition isArrLenLoc:: "Location ⇒ bool" where
"isArrLenLoc l = (case l of
                 objLoc cf a  ⇒ False 
               | staticLoc f     ⇒ False
               | arrLenLoc T a   ⇒ True
               | arrLoc T a i ⇒ False)"

lemma isArrLenLoc_simps [simp]:
"isArrLenLoc (objLoc cf a) = False" 
"isArrLenLoc (staticLoc f) = False"
"isArrLenLoc (arrLenLoc T a) = True"
"isArrLenLoc (arrLoc T a i) = False"
  by (simp_all add: isArrLenLoc_def)

definition isStaticLoc:: "Location ⇒ bool" where
"isStaticLoc l = (case l of
                 objLoc cff a ⇒ False
               | staticLoc f     ⇒ True
               | arrLenLoc T a   ⇒ False
               | arrLoc T a i ⇒ False)"
lemma isStaticLoc_simps [simp]:
"isStaticLoc (objLoc cf a) = False"
"isStaticLoc (staticLoc f)     = True"
"isStaticLoc (arrLenLoc T a)   = False"
"isStaticLoc (arrLoc T a i) = False"
  by (simp_all add: isStaticLoc_def)

text ‹The function ‹ref› yields the
object or array containing the location that is passed
as argument (see the function ‹obj› in 
\<^cite>‹‹p. 43 f.› in "Poetzsch-Heffter97specification"›).
Note that for static locations
the result is ‹nullV› since static locations 
are not associated to any object.
\label{ref_def}
›
definition ref:: "Location ⇒ Value" where
"ref l = (case l of
            objLoc cf a  ⇒ objV (cls cf) a
          | staticLoc f     ⇒ nullV
          | arrLenLoc T a   ⇒ arrV T a
          | arrLoc T a i ⇒ arrV T a)"

lemma ref_simps [simp]:
"ref (objLoc cf a)  = objV (cls cf) a"
"ref (staticLoc f)     = nullV"
"ref (arrLenLoc T a)   = arrV T a"
"ref (arrLoc T a i) = arrV T a"
  by (simp_all add: ref_def)

text ‹The function ‹loc› denotes the subscription of an object 
reference with an attribute.›
primrec loc:: "Value ⇒ AttId ⇒ Location"  ("_.._" [80,80] 80)
where "loc (objV c a) f = objLoc (catt c f) a"
text ‹Note that we only define subscription properly for object references.
For all other values we do not provide any defining equation, so they will 
internally be mapped to ‹arbitrary›.
›

text ‹The length of an array can be selected with the function ‹arr_len›.›
primrec arr_len:: "Value ⇒ Location"
where "arr_len (arrV T a) = arrLenLoc T a"

text ‹Arrays can be indexed by the function ‹arr_loc›.›
primrec arr_loc:: "Value ⇒ nat ⇒ Location" ("_.[_]" [80,80] 80)
where "arr_loc (arrV T a) i = arrLoc T a i" 

text ‹The functions @{term "loc"}, @{term "arr_len"} and @{term "arr_loc"}
define the interface between the basic store model (based on locations) and
the programming language Java. Instance field access {\tt obj.x} is modelled as 
@{term "obj..x"} or ‹loc obj x› (without the syntactic sugar), 
array length {\tt a.length} with @{term "arr_len a"},
array indexing {\tt a[i]} with @{term "a.[i]"} or ‹arr_loc a i›. 
The accessing of a static field 
{\tt C.f} can be expressed by the location itself ‹staticLoc C'f›.
Of course one can build more infrastructure to make access to instance fields
and static fields more uniform. We could for example define a 
function ‹static› which indicates whether a field is static or not and
based on that create an @{term "objLoc"} location or a @{term "staticLoc"} location. But 
this will only complicate the actual proofs and we can already easily 
perform the distinction whether a field is static or not in the \jive-frontend and 
therefore keep the verification simpler.
› 

lemma ref_loc [simp]: "⟦isObjV r; typeof r ≤ dtype f⟧ ⟹ ref (r..f) = r"
  apply (case_tac r)
  apply (case_tac [!] f)
  apply (simp_all)
  done

lemma obj_arr_loc [simp]: "isArrV r ⟹ ref (r.[i]) = r"
  by (cases r) simp_all

lemma obj_arr_len [simp]: "isArrV r ⟹ ref (arr_len r) = r"
  by (cases r) simp_all

end