Session JiveDataStoreModel

Theory TypeIds

(*  Title:       Jive Data and Store Model
    Author:      Nicole Rauch <rauch at informatik.uni-kl.de>, 2005
    Maintainer:  Nicole Rauch <rauch at informatik.uni-kl.de>
    License:     LGPL
*)

section ‹TypeIds›

theory TypeIds imports Main begin

text ‹\label{java_typeid_definitions}
This theory contains the program specific names of abstract and concrete classes and 
interfaces. It has to 
be generated for each program we want to verify. 
The following classes are an example taken from the program given in Sect. 
\ref{example-program}.
They are complemented by the classes that are known to exist in each Java program 
implicitly,
namely \texttt{Object}, \texttt{Exception}, \texttt{ClassCastException} and 
\texttt{NullPointerException}.
The example program does not contain any abstract classes, but since we cannot 
formalize datatypes without
constructors, we have to insert a dummy class which we call \texttt{Dummy}.

The datatype CTypeId must contain a constructor called \texttt{Object} because subsequent
proofs in the Subtype theory rely on it.
›

datatype CTypeId = CounterImpl | UndoCounter 
                 | Object | Exception | ClassCastException | NullPointerException
  ― ‹The last line contains the classes that exist in every program by default.›
datatype ITypeId = Counter
datatype ATypeId = Dummy
  ― ‹we cannot have an empty type.›

text ‹
Why do we need different datatypes for the different type identifiers?
Because we want to be able to distinguish the different identifier kinds.
This has a practical reason: If we formalize objects as "ObjectId $\times$ TypeId"
and if we quantify over all objects, we get a lot of objects that do not
exist, namely all objects that bear an interface type identifier or 
abstract class identifier. This is not very helpful. Therefore, we separate
the three identifier kinds from each other.
›




end

Theory JavaType

(*  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 ‹Java-Type›
 
theory JavaType imports "../Isa_Counter/TypeIds"
begin

text ‹This theory formalizes the types that appear in a Java program. Note that
the types defined by the classes and interfaces are formalized via their identifiers.
This way, this theory is program-independent.
›

text ‹We only want to formalize one-dimensional arrays. Therefore, we 
describe the types that can be used as element types of arrays. This excludes
the \texttt{null} type and array types themselves. This way, we get a finite 
number
of types in our type hierarchy, and the subtype relations can be given
explicitly (see Sec. \ref{direct_subtype_relations}). 
If desired, this can be extended in the future by using Javatype as argument
type of the ArrT› type constructor. This will yield infinitely many
types.
›

datatype Arraytype = BoolAT | IntgAT | ShortAT | ByteAT
                  | CClassAT CTypeId | AClassAT ATypeId
                  | InterfaceAT ITypeId

datatype Javatype = BoolT | IntgT | ShortT | ByteT | NullT | ArrT Arraytype
                  | CClassT CTypeId | AClassT ATypeId
                  | InterfaceT ITypeId

text ‹We need a function that widens @{typ Arraytype} to @{typ Javatype}.
›

definition
  at2jt :: "Arraytype  Javatype"
where
  "at2jt at = (case at of 
         BoolAT                BoolT
       | IntgAT                IntgT
       | ShortAT               ShortT
       | ByteAT                ByteT
       | CClassAT CTypeId      CClassT CTypeId
       | AClassAT ATypeId      AClassT ATypeId
       | InterfaceAT ITypeId   InterfaceT ITypeId)"
  
text ‹We define two predicates that separate the primitive types and the 
class types.
›
                             
primrec isprimitive:: "Javatype  bool"
where
"isprimitive BoolT = True" |
"isprimitive IntgT = True" |
"isprimitive ShortT = True" |
"isprimitive ByteT = True" |
"isprimitive NullT = False" |
"isprimitive (ArrT T) = False" |
"isprimitive (CClassT c) = False" |
"isprimitive (AClassT c) = False" |
"isprimitive (InterfaceT i) = False" 

primrec isclass:: "Javatype  bool"
where
"isclass BoolT = False" |
"isclass IntgT = False" |
"isclass ShortT = False" |
"isclass ByteT = False" |
"isclass NullT = False" |
"isclass (ArrT T) = False" |
"isclass (CClassT c) = True" |
"isclass (AClassT c) = True" |
"isclass (InterfaceT i) = False" 

end

Theory DirectSubtypes

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

section ‹The Direct Subtype Relation of Java Types›

theory DirectSubtypes
imports "../Isabelle/JavaType"
begin

text ‹
In this theory, we formalize the direct subtype relations of the Java types (as defined
in Sec. \ref{java_typeid_definitions}) that appear in the program to be verified. Thus, this
theory has to be generated for each program.
\label{direct_subtype_relations}
›

text ‹We have the following type hierarchy:
\begin{center}
\includegraphics[width=13cm]{TypeHierarchy}
\end{center}
We need to describe all direct subtype relations of this  type hierarchy.
As you can see in the picture, all unnecessary direct subtype relations can be
ignored, e.g. the subclass relation between CounterImpl and Object, because it is 
added
transitively by the widening relation of types (see Sec. \ref{widening_subtypes}).
›

text ‹
We have to specify the direct subtype relation between
\begin{itemize}
\item each ``leaf'' class or interface and its subtype \texttt{NullT}
\item each ``root'' class or interface and its supertype \texttt{Object}
\item each two types that are direct subtypes as specified in the code by
\texttt{extends} or \texttt{implements}
\item each array type of a primitive type and its subtype \texttt{NullT}
\item each array type of a primitive type and its supertype \texttt{Object}
\item each array type of a ``leaf'' class or interface and its subtype \texttt{NullT}
\item the array type \texttt{Object[]} and its supertype \texttt{Object}
\item two array types if their element types are in a subtype hierarchy
\end{itemize}
›

definition direct_subtype :: "(Javatype * Javatype) set" where
"direct_subtype =
{ (NullT, AClassT Dummy),
  (NullT, CClassT UndoCounter), 
  (NullT, CClassT NullPointerException),
  (NullT, CClassT ClassCastException),

  (AClassT Dummy, CClassT Object),
  (InterfaceT Counter, CClassT Object),
  (CClassT Exception, CClassT Object), 

  (CClassT UndoCounter, CClassT CounterImpl), 
  (CClassT CounterImpl, InterfaceT Counter),
  (CClassT NullPointerException, CClassT Exception),
  (CClassT ClassCastException, CClassT Exception),

  (NullT, ArrT BoolAT),
  (NullT, ArrT IntgAT),
  (NullT, ArrT ShortAT),
  (NullT, ArrT ByteAT),
  (ArrT BoolAT,  CClassT Object),
  (ArrT IntgAT,  CClassT Object),
  (ArrT ShortAT, CClassT Object),
  (ArrT ByteAT,  CClassT Object),

  (NullT, ArrT (AClassAT Dummy)),
  (NullT, ArrT (CClassAT UndoCounter)),
  (NullT, ArrT (CClassAT NullPointerException)),
  (NullT, ArrT (CClassAT ClassCastException)),

  (ArrT (CClassAT Object),      CClassT Object),

  (ArrT (AClassAT Dummy),       ArrT (CClassAT Object)),
  (ArrT (CClassAT CounterImpl), ArrT (InterfaceAT Counter)), 
  (ArrT (InterfaceAT Counter),  ArrT (CClassAT Object)),
  (ArrT (CClassAT Exception),   ArrT (CClassAT Object)), 
  (ArrT (CClassAT UndoCounter), ArrT (CClassAT CounterImpl)), 
  (ArrT (CClassAT NullPointerException), ArrT (CClassAT Exception)),
  (ArrT (CClassAT ClassCastException),   ArrT (CClassAT Exception))
}"

text ‹This lemma is used later in the Simplifier.›

lemma direct_subtype:
  "(NullT, AClassT Dummy)  direct_subtype"
  "(NullT, CClassT UndoCounter)  direct_subtype" 
  "(NullT, CClassT NullPointerException)  direct_subtype"
  "(NullT, CClassT ClassCastException)  direct_subtype"

  "(AClassT Dummy, CClassT Object)  direct_subtype"
  "(InterfaceT Counter, CClassT Object)  direct_subtype"
  "(CClassT Exception, CClassT Object)  direct_subtype" 

  "(CClassT UndoCounter, CClassT CounterImpl)  direct_subtype" 
  "(CClassT CounterImpl, InterfaceT Counter)  direct_subtype"
  "(CClassT NullPointerException, CClassT Exception)  direct_subtype"
  "(CClassT ClassCastException, CClassT Exception)  direct_subtype"

  "(NullT, ArrT BoolAT)  direct_subtype"
  "(NullT, ArrT IntgAT)  direct_subtype"
  "(NullT, ArrT ShortAT)  direct_subtype"
  "(NullT, ArrT ByteAT)  direct_subtype"
  "(ArrT BoolAT,  CClassT Object)  direct_subtype"
  "(ArrT IntgAT,  CClassT Object)  direct_subtype"
  "(ArrT ShortAT, CClassT Object)  direct_subtype"
  "(ArrT ByteAT,  CClassT Object)  direct_subtype"

  "(NullT, ArrT (AClassAT Dummy))  direct_subtype"
  "(NullT, ArrT (CClassAT UndoCounter))  direct_subtype"
  "(NullT, ArrT (CClassAT NullPointerException))  direct_subtype"
  "(NullT, ArrT (CClassAT ClassCastException))  direct_subtype"

  "(ArrT (CClassAT Object),      CClassT Object)  direct_subtype"

  "(ArrT (AClassAT Dummy),       ArrT (CClassAT Object))  direct_subtype"
  "(ArrT (CClassAT CounterImpl), ArrT (InterfaceAT Counter))  direct_subtype" 
  "(ArrT (InterfaceAT Counter),  ArrT (CClassAT Object))  direct_subtype"
  "(ArrT (CClassAT Exception),   ArrT (CClassAT Object))  direct_subtype" 
  "(ArrT (CClassAT UndoCounter), ArrT (CClassAT CounterImpl))  direct_subtype" 
  "(ArrT (CClassAT NullPointerException), ArrT (CClassAT Exception))  direct_subtype"
  "(ArrT (CClassAT ClassCastException),   ArrT (CClassAT Exception))  direct_subtype"
  by (simp_all add: direct_subtype_def)

end

Theory Subtype

(*  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 ‹Widening the Direct Subtype Relation›

theory Subtype
imports "../Isa_Counter/DirectSubtypes"
begin

text ‹
In this theory, we define the widening subtype relation of types and prove 
that it is a partial order.
›

subsection ‹Auxiliary lemmas›

text ‹These general lemmas are not especially related to Jive. 
They capture
some useful properties of general relations. 
›
lemma distinct_rtrancl_into_trancl:
  assumes neq_x_y: "xy"
  assumes x_y_rtrancl: "(x,y)  r*"
  shows "(x,y)  r+"
  using x_y_rtrancl neq_x_y
proof (induct)
  assume "xx" thus "(x, x)  r+" by simp
next
  fix y z
  assume x_y_rtrancl: "(x, y)  r*" 
  assume y_z_r: "(y, z)  r" 
  assume "x  y  (x, y)  r+" 
  assume "x  z"
  from x_y_rtrancl
  show "(x, z)  r+"
  proof (cases)
    assume "x=y"
    with y_z_r have "(x,z)  r" by simp
    thus "(x,z)   r+"..
  next
    fix w
    assume "(x, w)  r*"
    moreover assume "(w, y)  r"
    ultimately have "(x,y)  r+"
      by (rule rtrancl_into_trancl1)
    from this y_z_r
    show "(x, z)  r+"..
  qed
qed

lemma acyclic_imp_antisym_rtrancl: "acyclic r  antisym (r*)"
proof (clarsimp simp only: acyclic_def antisym_def)
  fix x y
  assume acyclic: "x. (x, x)  r+"
  assume x_y: "(x, y)  r*" 
  assume y_x: "(y, x)  r*"
  show "x=y"
  proof (cases "x=y")
    case True thus ?thesis .
  next
    case False
    from False x_y have "(x, y)  r+"
      by (rule distinct_rtrancl_into_trancl)
    also
    from False y_x have "(y, x)  r+"
      by (fastforce intro: distinct_rtrancl_into_trancl)
    finally have "(x,x)  r+".
    with acyclic show ?thesis by simp
  qed
qed

lemma acyclic_trancl_rtrancl: 
  assumes acyclic: "acyclic r"
  shows "(x,y)  r+ = ((x,y)  r*  xy)"
proof
  assume x_y_trancl: "(x,y)  r+"
  show "(x,y)  r*  xy"
  proof
    from x_y_trancl show "(x,y)  r*"..
  next
    from x_y_trancl acyclic show "xy" by (auto simp add: acyclic_def)
  qed
next
  assume "(x,y)  r*  xy"
  thus "(x,y)  r+"
    by (auto intro: distinct_rtrancl_into_trancl)
qed


subsection ‹The Widening (Subtype) Relation of Javatypes›


text ‹\label{widening_subtypes}
In this section we widen the direct subtype relations specified in Sec. 
\ref{direct_subtype_relations}.
It is done by a calculation of the transitive closure of the 
direct subtype relation. 
›

text ‹This is the concrete syntax that expresses the subtype relations 
between all types. 
\label{subtype_relations_concrete_syntax}›

abbreviation
  direct_subtype_syntax :: "Javatype  Javatype  bool" ("_ ≺1 _" [71,71] 70)
where ― ‹direct subtype relation›
  "A ≺1 B == (A,B)  direct_subtype"

abbreviation
  widen_syntax :: "Javatype  Javatype  bool" ("_  _" [71,71] 70)
where ― ‹reflexive transitive closure of direct subtype relation›
  "A  B == (A,B)  direct_subtype*"

abbreviation
  widen_strict_syntax :: "Javatype  Javatype  bool" ("_  _" [71,71] 70)
where ― ‹transitive closure of direct subtype relation›
  "A  B == (A,B)  direct_subtype+"


subsection ‹The Subtype Relation as Partial Order›

text ‹We prove the axioms required for partial orders, i.e.\ 
reflexivity, transitivity and antisymmetry, for the widened subtype
relation. The direct subtype relation has been
defined in Sec. \ref{direct_subtype_relations}.
The reflexivity lemma is
added to the Simplifier and to the Classical reasoner (via the
attribute iff), and the transitivity and antisymmetry lemmas
are made known as transitivity rules (via the attribute trans).
This way, these lemmas will be automatically used in subsequent proofs.
›

lemma acyclic_direct_subtype: "acyclic direct_subtype"
proof (clarsimp simp add: acyclic_def)
  fix x show "x  x  False"
  by (cases x) (fastforce elim: tranclE simp add: direct_subtype_def)+
     (* takes a very long time to calculate *)
qed

lemma antisym_rtrancl_direct_subtype: "antisym (direct_subtype*)"
using acyclic_direct_subtype by (rule acyclic_imp_antisym_rtrancl)

lemma widen_strict_to_widen: "C  D = (C  D  CD)"
using acyclic_direct_subtype by (rule acyclic_trancl_rtrancl)

text ‹The widening relation on Javatype is reflexive.›

lemma widen_refl [iff]: "X  X" ..

text ‹The widening relation on Javatype is transitive.›

lemma widen_trans [trans] : 
  assumes a_b: "a  b"
  shows " c. b  c  a  c"
  by (insert a_b, rule rtrancl_trans)

text ‹The widening relation on Javatype is antisymmetric.›

lemma widen_antisym [trans]: 
  assumes a_b: "a  b" 
  assumes b_c: "b  a"  
  shows "a = b"
  using a_b b_c antisym_rtrancl_direct_subtype
  by (unfold antisym_def) blast


subsection ‹Javatype Ordering Properties›

text ‹The type class @{term ord} allows us to overwrite the two comparison 
operators $<$ and $\leq$.
  These are  the two comparison operators on @{typ Javatype} that we want
to use subsequently.›

text ‹We can also prove that @{typ Javatype} is in the type class @{term order}. 
For this we
  have to prove reflexivity, transitivity, antisymmetry and that $<$ and $\leq$ are 
defined in such
  a way that @{thm Orderings.order_less_le [no_vars]} holds. This proof can easily 
be achieved by using the
  lemmas proved above and the definition of @{term less_Javatype_def}.
›

instantiation Javatype:: order
begin

definition
  le_Javatype_def:   "A  B  A  B"

definition
  less_Javatype_def: "A < B  A  B  ¬ B  (A::Javatype)"
  
instance proof
  fix x y z:: "Javatype"
  {
    show "x  x"
      by (simp add: le_Javatype_def )
  next
    assume "x  y" "y  z"
    then show "x  z"
      by (unfold le_Javatype_def) (rule rtrancl_trans) 
  next
    assume "x  y" "y  x" 
    then show "x = y"
      apply (unfold le_Javatype_def) 
      apply (rule widen_antisym) 
      apply assumption +
      done
  next
    show "(x < y) = (x  y  ¬ y  x)"
      by (simp add: less_Javatype_def)
  }
qed

end


subsection ‹Enhancing the Simplifier›

lemmas subtype_defs = le_Javatype_def less_Javatype_def
                      direct_subtype_def 
(*
                      direct_subtype
                      direct_subtype[THEN r_into_rtrancl]
*)
lemmas subtype_ok_simps = subtype_defs 
lemmas subtype_wrong_elims = rtranclE

text ‹During verification we will often have to solve the goal that one type
widens to the other. So we equip the simplifier with a special solver-tactic.
›

lemma widen_asm: "(a::Javatype)  b  a  b"
  by simp

lemmas direct_subtype_widened = direct_subtype[THEN r_into_rtrancl]

ML local val ss = simpset_of @{context} in

fun widen_tac ctxt =
  resolve_tac ctxt @{thms widen_asm} THEN'
  simp_tac (put_simpset ss ctxt addsimps @{thms le_Javatype_def}) THEN'
  Method.insert_tac ctxt @{thms direct_subtype_widened} THEN'
  simp_tac (put_simpset (simpset_of @{theory_context Transitive_Closure}) ctxt)

end

declaration fn _ =>
  Simplifier.map_ss (fn ss => ss addSolver (mk_solver "widen" widen_tac))


text ‹In this solver-tactic, we first try the trivial resolution with widen_asm› to
check if the actual subgaol really is a request to solve a subtyping problem.
If so, we unfold the comparison operator, insert the direct subtype
relations and call the simplifier.
›


subsection ‹Properties of the Subtype Relation›


text ‹The class Object› has to be the root of the class hierarchy, 
i.e.~it is supertype of each concrete class, abstract class, interface
and array type.
  The proof scripts should run on every correctly generated type hierarchy.
›


lemma Object_root: "CClassT C  CClassT Object"
  by (cases C, simp_all)

lemma Object_root_abs: "AClassT C  CClassT Object"
  by (cases C, simp_all)

lemma Object_root_int: "InterfaceT C  CClassT Object"
  by (cases C, simp_all)

lemma Object_root_array: "ArrT C  CClassT Object"
  proof (cases C)
    fix x
    assume c: "C = CClassAT x"
    show "ArrT C  CClassT Object"
      using c by (cases x, simp_all)
  next
    fix x
    assume c: "C = AClassAT x"
    show "ArrT C  CClassT Object"
      using c by (cases x, simp_all)
  next
    fix x
    assume c: "C = InterfaceAT x"
    show "ArrT C  CClassT Object"
      using c by (cases x, simp_all)
  next
    assume c: "C = BoolAT"
    show "ArrT C  CClassT Object"
      using c by simp
  next
    assume c: "C = IntgAT"
    show "ArrT C  CClassT Object"
      using c by simp
  next
    assume c: "C = ShortAT"
    show "ArrT C  CClassT Object"
      using c by simp
  next
    assume c: "C = ByteAT"
    show "ArrT C  CClassT Object"
      using c by simp
qed

text ‹If another type is (non-strict) supertype of Object, 
then it must be the type Object itself.›

lemma Object_rootD: 
  assumes p: "CClassT Object  c"
  shows "CClassT Object = c"
  using p
  apply (cases c)
  apply (fastforce elim: subtype_wrong_elims simp add: subtype_defs) +
  ― ‹In this lemma, we only get contradictory cases except for Object itself.›
done

text ‹The type NullT has to be the leaf of each branch of the class
hierarchy, i.e.~it is subtype of each type.›

lemma NullT_leaf [simp]: "NullT  CClassT C"
  by (cases C, simp_all)

lemma NullT_leaf_abs [simp]: "NullT  AClassT C"
  by (cases C, simp_all)

lemma NullT_leaf_int [simp]: "NullT  InterfaceT C"
  by (cases C, simp_all)

lemma NullT_leaf_array: "NullT  ArrT C"
  proof (cases C)
    fix x
    assume c: "C = CClassAT x"
    show "NullT  ArrT C"
      using c by (cases x, simp_all)
  next
    fix x
    assume c: "C = AClassAT x"
    show "NullT  ArrT C"
      using c by (cases x, simp_all)
  next
    fix x
    assume c: "C = InterfaceAT x"
    show "NullT  ArrT C"
      using c by (cases x, simp_all)
  next
    assume c: "C = BoolAT"
    show "NullT  ArrT C"
      using c by simp
  next
    assume c: "C = IntgAT"
    show "NullT  ArrT C"
      using c by simp
  next
    assume c: "C = ShortAT"
    show "NullT  ArrT C"
      using c by simp
  next
    assume c: "C = ByteAT"
    show "NullT  ArrT C"
      using c by simp
qed

end

Theory Attributes

(*  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 ‹Attributes›

theory Attributes
imports "../Isabelle/Subtype"
begin

text ‹This theory has to be generated as well for each program under 
verification. It defines the attributes of the classes and various functions
on them.
›

datatype AttId = CounterImpl'value | UndoCounter'save
  | Dummy'dummy | Counter'dummy

text ‹The last two entries are only added to demonstrate what is to happen with attributes of
abstract classes and interfaces.›

text  ‹It would be nice if attribute names were generated in a way that keeps them short, so that the proof
state does not get unreadable because of fancy long names. The generation of 
attribute names that is performed by the
Jive tool should only add the definition class if necessary, i.e.~if there 
 would be a name clash otherwise. For the example above, the class names are not 
necessary. One must be careful, though, not to generate names that might clash with names of free variables
that are used subsequently.
›

text ‹The domain type of an attribute is the definition class (or interface)
of the attribute.›
definition dtype:: "AttId  Javatype" where
"dtype f = (case f of 
              CounterImpl'value  CClassT CounterImpl
            | UndoCounter'save  CClassT UndoCounter
            | Dummy'dummy  AClassT Dummy
            | Counter'dummy  InterfaceT Counter)"

lemma dtype_simps [simp]:
"dtype CounterImpl'value = CClassT CounterImpl" 
"dtype UndoCounter'save = CClassT UndoCounter"
"dtype Dummy'dummy = AClassT Dummy"
"dtype Counter'dummy = InterfaceT Counter"
  by (simp_all add: dtype_def dtype_def dtype_def)

text ‹For convenience, we add some functions that directly apply the selectors of 
  the datatype @{typ Javatype}.
›
  
definition cDTypeId :: "AttId  CTypeId" where
"cDTypeId f = (case f of 
              CounterImpl'value  CounterImpl
            | UndoCounter'save  UndoCounter
            | Dummy'dummy  undefined
            | Counter'dummy  undefined )"

definition aDTypeId:: "AttId  ATypeId" where
"aDTypeId f = (case f of 
              CounterImpl'value  undefined
            | UndoCounter'save  undefined
            | Dummy'dummy  Dummy
            | Counter'dummy  undefined )"

definition iDTypeId:: "AttId  ITypeId" where
"iDTypeId f = (case f of 
              CounterImpl'value  undefined
            | UndoCounter'save  undefined
            | Dummy'dummy  undefined
            | Counter'dummy  Counter )"

lemma DTypeId_simps [simp]:
"cDTypeId CounterImpl'value = CounterImpl" 
"cDTypeId UndoCounter'save = UndoCounter"
"aDTypeId Dummy'dummy = Dummy"
"iDTypeId Counter'dummy = Counter"
  by (simp_all add: cDTypeId_def aDTypeId_def iDTypeId_def)


text ‹The range type of an attribute is the type of the value stored in that
attribute.
›
definition rtype:: "AttId  Javatype" where
"rtype f = (case f of 
              CounterImpl'value  IntgT
            | UndoCounter'save  IntgT
            | Dummy'dummy  NullT
            | Counter'dummy  NullT)"

lemma rtype_simps [simp]:
"rtype CounterImpl'value  = IntgT"
"rtype UndoCounter'save  = IntgT"
"rtype Dummy'dummy = NullT"
"rtype Counter'dummy = NullT"
  by (simp_all add: rtype_def rtype_def rtype_def)

text ‹With the datatype CAttId› we describe the possible locations 
in memory for
instance fields. We rule out the impossible combinations of class names and
field names. For example, a CounterImpl› cannot have a save› 
field. A store model which provides locations for all possible combinations
of the Cartesian product of class name and field name works out fine as 
well, because we cannot express modification of such ``wrong'' 
locations in a Java program. So we can only prove useful properties about 
reasonable combinations.
The only drawback in such a model is that we cannot prove a property like 
not_treach_ref_impl_not_reach› in theory StoreProperties. 
If the store provides locations for
every combination of class name and field name, we cannot rule out 
reachability of certain pointer chains that go through ``wrong'' locations. 
That is why we decided to introduce the new type CAttId›.

  While AttId› describes which fields 
are declared in which classes and interfaces,
  CAttId› describes which objects of which classes may contain which 
fields at run-time. Thus,
  CAttId› makes the inheritance of fields visible in the formalization.

There is only one such datatype because only objects of concrete classes can be 
created at run-time,
thus only instance fields of concrete classes can occupy memory.›

  datatype CAttId = CounterImpl'CounterImpl'value | UndoCounter'CounterImpl'value
  | UndoCounter'UndoCounter'save 
  | CounterImpl'Counter'dummy | UndoCounter'Counter'dummy


text ‹Function catt› builds a CAttId› from a class name
and a field name. In case of the illegal combinations we just return
undefined›. We can also filter out static fields in 
catt›.›
  
definition catt:: "CTypeId  AttId  CAttId" where
"catt C f =
  (case C of
     CounterImpl  (case f of 
                CounterImpl'value  CounterImpl'CounterImpl'value
              | UndoCounter'save  undefined
              | Dummy'dummy  undefined
              | Counter'dummy  CounterImpl'Counter'dummy)
   | UndoCounter  (case f of 
                     CounterImpl'value  UndoCounter'CounterImpl'value
                   | UndoCounter'save  UndoCounter'UndoCounter'save
                   | Dummy'dummy  undefined
                   | Counter'dummy  UndoCounter'Counter'dummy)
   | Object  undefined
   | Exception  undefined
   | ClassCastException  undefined
   | NullPointerException  undefined
)"


lemma catt_simps [simp]:
"catt CounterImpl CounterImpl'value = CounterImpl'CounterImpl'value"
"catt UndoCounter CounterImpl'value = UndoCounter'CounterImpl'value"
"catt UndoCounter UndoCounter'save = UndoCounter'UndoCounter'save"
"catt CounterImpl Counter'dummy = CounterImpl'Counter'dummy"
"catt UndoCounter Counter'dummy = UndoCounter'Counter'dummy"
  by (simp_all add: catt_def)

text ‹Selection of the class name of the type of the object in which the field lives.
  The field can only be located in a concrete class.›
  
definition cls:: "CAttId  CTypeId" where
"cls cf = (case cf of
             CounterImpl'CounterImpl'value   CounterImpl
           | UndoCounter'CounterImpl'value   UndoCounter
           | UndoCounter'UndoCounter'save   UndoCounter
  | CounterImpl'Counter'dummy  CounterImpl
  | UndoCounter'Counter'dummy  UndoCounter
)"

lemma cls_simps [simp]:
"cls CounterImpl'CounterImpl'value = CounterImpl"
"cls UndoCounter'CounterImpl'value = UndoCounter"
"cls UndoCounter'UndoCounter'save = UndoCounter"
"cls CounterImpl'Counter'dummy = CounterImpl"
"cls UndoCounter'Counter'dummy = UndoCounter"
  by (simp_all add: cls_def)

text ‹Selection of the field name.›
definition att:: "CAttId  AttId" where
"att cf = (case cf of
             CounterImpl'CounterImpl'value   CounterImpl'value
           | UndoCounter'CounterImpl'value   CounterImpl'value
           | UndoCounter'UndoCounter'save   UndoCounter'save
           | CounterImpl'Counter'dummy  Counter'dummy
           | UndoCounter'Counter'dummy  Counter'dummy
)"

lemma att_simps [simp]:
"att CounterImpl'CounterImpl'value = CounterImpl'value"
"att UndoCounter'CounterImpl'value = CounterImpl'value"
"att UndoCounter'UndoCounter'save = UndoCounter'save"
"att CounterImpl'Counter'dummy = Counter'dummy"
"att UndoCounter'Counter'dummy = Counter'dummy"
  by (simp_all add: att_def)

end

Theory AttributesIndep

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

section ‹Program-Independent Lemmas on Attributes›

theory AttributesIndep
imports "../Isa_Counter_Store/Attributes"
begin

text ‹The following lemmas validate the functions defined in the Attributes theory.
They also aid in subsequent proving tasks. Since they are
program-independent, it is of no use to add them to the generation process of
Attributes.thy. Therefore, they have been extracted to this theory.
›

lemma cls_catt [simp]: 
  "CClassT c  dtype f  cls (catt c f) = c"
  apply (case_tac c)
  apply (case_tac [!] f)
  apply simp_all
   ― ‹solves all goals where @{text "CClassT c ≤ dtype f"}
  apply (fastforce elim: subtype_wrong_elims simp add: subtype_defs)+
   ― ‹solves all the rest where @{text "¬ CClassT c ≤ dtype f"} can be derived›
  done

lemma att_catt [simp]: 
  "CClassT c  dtype f  att (catt c f) = f"
  apply (case_tac c)
  apply (case_tac [!] f)
  apply simp_all
   ― ‹solves all goals where @{text "CClassT c ≤ dtype f"}
  apply (fastforce elim: subtype_wrong_elims simp add: subtype_defs)+
   ― ‹solves all the rest where @{text "¬ CClassT c ≤ dtype f"} can be 
        derived›
  done

text ‹The following lemmas are just a demonstration of simplification.›

lemma rtype_att_catt: 
  "CClassT c  dtype f  rtype (att (catt c f)) = rtype f"
  by simp

lemma widen_cls_dtype_att [simp,intro]: 
  "(CClassT (cls cf)  dtype (att cf)) "
  by (cases cf, simp_all)

end

Theory Value

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

theory Value imports Subtype begin

text ‹This theory contains our model of the values in the store. The store is untyped, therefore all
  types that exist in Java are wrapped into one type Value›.

  In a first approach, the primitive Java types supported in this formalization are 
  mapped to similar Isabelle
  types. Later, we will have
  proper formalizations of the Java types in Isabelle, which will then be used here.
›
  
type_synonym JavaInt = int
type_synonym JavaShort = int
type_synonym JavaByte = int
type_synonym JavaBoolean = bool

text ‹The objects of each class are identified by a unique ID.
We use elements of type @{typ nat} here, but in general it is sufficient to use
an infinite type with a successor function and a comparison predicate.
›

type_synonym ObjectId = nat

text ‹The definition of the datatype Value›. Values can be of the Java types 
boolean, int, short and byte. Additionally, they can be an object reference,
an array reference or the value null.›

datatype Value = boolV  JavaBoolean
               | intgV  JavaInt  
               | shortV JavaShort
               | byteV  JavaByte
               | objV   CTypeId ObjectId   ― ‹typed object reference›
               | arrV   Arraytype ObjectId ― ‹typed array reference›
               | nullV
               

text ‹Arrays are modeled as references just like objects. So they
can be viewed as special kinds of objects, like in Java.›

subsection ‹Discriminator Functions›

text ‹To test values, we define the following discriminator functions.›

definition isBoolV  :: "Value  bool" where
"isBoolV v = (case v of
               boolV b   True 
             | intgV i   False
             | shortV s  False
             | byteV  by  False
             | objV C a  False
             | arrV T a  False
             | nullV     False)"

lemma isBoolV_simps [simp]:
"isBoolV (boolV b)       = True" 
"isBoolV (intgV i)       = False"
"isBoolV (shortV s)      = False"
"isBoolV (byteV by)       = False"
"isBoolV (objV C a)      = False"
"isBoolV (arrV T a)      = False"
"isBoolV (nullV)         = False"
  by (simp_all add: isBoolV_def)


definition isIntgV  :: "Value  bool" where
"isIntgV v = (case v of
               boolV b   False 
             | intgV i   True
             | shortV s  False
             | byteV by   False
             | objV C a  False
             | arrV T a  False
             | nullV     False)" 

lemma isIntgV_simps [simp]:
"isIntgV (boolV b)       = False" 
"isIntgV (intgV i)       = True"
"isIntgV (shortV s)       = False"
"isIntgV (byteV by)       = False"
"isIntgV (objV C a)      = False"
"isIntgV (arrV T a)      = False"
"isIntgV (nullV)         = False"
  by (simp_all add: isIntgV_def)


definition isShortV :: "Value  bool" where
"isShortV v = (case v of
               boolV b   False 
             | intgV i   False
             | shortV s  True
             | byteV by   False
             | objV C a  False
             | arrV T a  False
             | nullV     False)" 

lemma isShortV_simps [simp]:
"isShortV (boolV b)     = False" 
"isShortV (intgV i)     = False"
"isShortV (shortV s)    = True"
"isShortV (byteV by)     = False"
"isShortV (objV C a)    = False"
"isShortV (arrV T a)    = False"
"isShortV (nullV)       = False"
  by (simp_all add: isShortV_def)


definition isByteV :: "Value  bool" where
"isByteV v = (case v of
               boolV b   False 
             | intgV i   False
             | shortV s  False
             | byteV by   True
             | objV C a  False
             | arrV T a  False
             | nullV     False)" 

lemma isByteV_simps [simp]:
"isByteV (boolV b)      = False" 
"isByteV (intgV i)      = False"
"isByteV (shortV s)     = False"
"isByteV (byteV by)      = True"
"isByteV (objV C a)     = False"
"isByteV (arrV T a)     = False"
"isByteV (nullV)        = False"
  by (simp_all add: isByteV_def)


definition isRefV :: "Value  bool" where
"isRefV v = (case v of
               boolV b   False 
             | intgV i   False
             | shortV s  False
             | byteV by  False
             | objV C a   True
             | arrV T a   True
             | nullV      True)"

lemma isRefV_simps [simp]:
"isRefV (boolV b)       = False" 
"isRefV (intgV i)       = False"
"isRefV (shortV s)      = False"
"isRefV (byteV by)      = False"
"isRefV (objV C a)      = True"
"isRefV (arrV T a)      = True"
"isRefV (nullV)         = True"
  by (simp_all add: isRefV_def)


definition isObjV :: "Value  bool" where
"isObjV v = (case v of
               boolV b   False 
             | intgV i   False
             | shortV s   False
             | byteV by   False
             | objV C a  True
             | arrV T a  False
             | nullV     False)"

lemma isObjV_simps [simp]:
"isObjV (boolV b)  = False" 
"isObjV (intgV i)  = False"
"isObjV (shortV s)  = False"
"isObjV (byteV by)  = False"
"isObjV (objV c a) = True" 
"isObjV (arrV T a) = False"
"isObjV nullV      = False"
  by (simp_all add: isObjV_def)


definition isArrV :: "Value  bool" where
"isArrV v = (case v of
               boolV b   False 
             | intgV i   False
             | shortV s   False
             | byteV by   False
             | objV C a  False
             | arrV T a  True
             | nullV     False)"

lemma isArrV_simps [simp]:
"isArrV (boolV b)  = False" 
"isArrV (intgV i)  = False"
"isArrV (shortV s)  = False"
"isArrV (byteV by)  = False"
"isArrV (objV c a) = False" 
"isArrV (arrV T a) = True"
"isArrV nullV      = False"
  by (simp_all add: isArrV_def)


definition isNullV  :: "Value  bool" where
"isNullV v = (case v of
               boolV b   False 
             | intgV i   False
             | shortV s   False
             | byteV by   False
             | objV C a  False
             | arrV T a  False
             | nullV     True)"

lemma isNullV_simps [simp]:
"isNullV (boolV b)   = False" 
"isNullV (intgV i)   = False"
"isNullV (shortV s)   = False"
"isNullV (byteV by)   = False"
"isNullV (objV c a) = False" 
"isNullV (arrV T a) = False"
"isNullV nullV      = True"
  by (simp_all add: isNullV_def)

subsection ‹Selector Functions›

definition aI :: "Value  JavaInt" where
"aI v = (case v of  
            boolV  b    undefined
          | intgV  i    i
          | shortV sh   undefined
          | byteV  by   undefined
          | objV   C a  undefined
          | arrV  T a   undefined
          | nullV       undefined)"
lemma aI_simps [simp]:
"aI (intgV i) = i"
by (simp add: aI_def)


definition aB :: "Value  JavaBoolean" where
"aB v = (case v of  
            boolV  b    b
          | intgV  i    undefined
          | shortV sh   undefined
          | byteV  by   undefined
          | objV   C a  undefined
          | arrV  T a   undefined
          | nullV       undefined)"
lemma aB_simps [simp]:
"aB (boolV b) = b"
by (simp add: aB_def)


definition aSh :: "Value  JavaShort" where
"aSh v = (case v of  
            boolV  b    undefined
          | intgV  i    undefined
          | shortV sh   sh
          | byteV  by   undefined
          | objV   C a  undefined
          | arrV  T a   undefined
          | nullV       undefined)"
lemma aSh_simps [simp]:
"aSh (shortV sh) = sh"
by (simp add: aSh_def)


definition aBy :: "Value  JavaByte" where
"aBy v = (case v of  
            boolV  b    undefined
          | intgV  i    undefined
          | shortV s    undefined
          | byteV  by   by
          | objV   C a  undefined
          | arrV  T a   undefined
          | nullV       undefined)"
lemma aBy_simps [simp]:
"aBy (byteV by) = by"
by (simp add: aBy_def)


definition tid :: "Value  CTypeId" where
"tid v = (case v of
            boolV  b    undefined
          | intgV  i    undefined
          | shortV s    undefined
          | byteV  by   undefined
          | objV   C a  C
          | arrV  T a   undefined
          | nullV       undefined)"

lemma tid_simps [simp]:
"tid (objV C a) = C"
by (simp add: tid_def)


definition oid :: "Value  ObjectId" where
"oid v = (case v of
            boolV  b    undefined
          | intgV  i    undefined
          | shortV s    undefined
          | byteV  by   undefined
          | objV   C a  a
          | arrV  T a   undefined
          | nullV       undefined)"

lemma oid_simps [simp]:
"oid (objV C a) = a"
by (simp add: oid_def)


definition jt :: "Value  Javatype" where
"jt v = (case v of
            boolV  b    undefined
          | intgV  i    undefined
          | shortV s    undefined
          | byteV  by   undefined
          | objV   C a  undefined
          | arrV  T a   at2jt T
          | nullV       undefined)"

lemma jt_simps [simp]:
"jt (arrV T a) = at2jt T"
by (simp add: jt_def)


definition aid :: "Value  ObjectId" where
"aid v = (case v of
            boolV  b    undefined
          | intgV  i    undefined
          | shortV s    undefined
          | byteV  by   undefined
          | objV   C a  undefined
          | arrV  T a   a
          | nullV       undefined)"

lemma aid_simps [simp]:
"aid (arrV T a) = a"
by (simp add: aid_def)

subsection‹Determining the Type of a Value›

text ‹To determine the type of a value, we define the function
typeof›. This function is
often written as $\tau$ in theoretical texts, therefore we add
the appropriate syntax support.›

definition typeof :: "Value  Javatype" where
"typeof v = (case v of
               boolV b   BoolT 
             | intgV i   IntgT
             | shortV sh   ShortT
             | byteV by   ByteT
             | objV C a  CClassT C
             | arrV T a  ArrT T
             | nullV     NullT)"

abbreviation tau_syntax :: "Value  Javatype" ("τ _")
  where "τ v == typeof v"

lemma typeof_simps [simp]:
"(τ (boolV b)) = BoolT"
"(τ (intgV i)) = IntgT"
"(τ (shortV sh)) = ShortT"
"(τ (byteV by)) = ByteT"
"(τ (objV c a)) = CClassT c"
"(τ (arrV t a)) = ArrT t"
"(τ (nullV))   = NullT"
  by (simp_all add: typeof_def)


subsection ‹Default Initialization Values for Types›

text ‹The function init› yields the default initialization values for each 
type. For boolean, the
default value is False, for the integral types, it is 0, and for the reference
types, it is nullV.
›

definition init :: "Javatype  Value" where
"init T = (case T of
             BoolT         boolV  False
           | IntgT         intgV  0
           | ShortT         shortV 0
           | ByteT         byteV  0
           | NullT         nullV
           | ArrT T        nullV
           | CClassT C      nullV
           | AClassT C      nullV
           | InterfaceT I  nullV)" 

lemma init_simps [simp]:
"init BoolT          = boolV False"
"init IntgT          = intgV 0"
"init ShortT         = shortV 0"
"init ByteT          = byteV 0"
"init NullT          = nullV"
"init (ArrT T)       = nullV"
"init (CClassT c)     = nullV"
"init (AClassT a)     = nullV"
"init (InterfaceT i) = nullV"
  by (simp_all add: init_def)

lemma typeof_init_widen [simp,intro]: "typeof (init T)  T"
proof (cases T)
  assume c: "T = BoolT"
  show "(τ (init T))  T"
    using c by simp
next
  assume c: "T = IntgT"
  show "(τ (init T))  T"
    using c by simp
next
  assume c: "T = ShortT"
  show "(τ (init T))  T"
    using c by simp
next
  assume c: "T = ByteT"
  show "(τ (init T))  T"
    using c by simp
next
  assume c: "T = NullT"
  show "(τ (init T))  T"
    using c by simp
next
  fix x
  assume c: "T = CClassT x"
  show "(τ (init T))  T"
    using c by (cases x, simp_all)
next
  fix x
  assume c: "T = AClassT x"
  show "(τ (init T))  T"
    using c by (cases x, simp_all)
next
  fix x
  assume c: "T = InterfaceT x"
  show "(τ (init T))  T"
    using c by (cases x, simp_all)
next
  fix x
  assume c: "T = ArrT x"
  show "(τ (init T))  T"
    using c 
  proof (cases x)
    fix y
    assume c2: "x = CClassAT y"
    show "(τ (init T))  T"
      using c c2 by (cases y, simp_all)
  next
    fix y
    assume c2: "x = AClassAT y"
    show "(τ (init T))  T"
      using c c2 by (cases y, simp_all)
  next
    fix y
    assume c2: "x = InterfaceAT y"
    show "(τ (init T))  T"
      using c c2 by (cases y, simp_all)
  next
    assume c2: "x = BoolAT"
    show "(τ (init T))  T"
      using c c2 by simp
  next
    assume c2: "x = IntgAT"
    show "(τ (init T))  T"
      using c c2 by simp
  next
    assume c2: "x = ShortAT"
    show "(τ (init T))  T"
      using c c2 by simp
  next
    assume c2: "x = ByteAT"
    show "(τ (init T))  T"
      using c c2 by simp
  qed
qed

end

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.]{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

Theory Store

(*  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 ‹Store›

theory Store
imports Location
begin

subsection ‹New›
text ‹The store provides a uniform interface to allocate new objects and
new arrays. The constructors of this datatype distinguish both cases.
›
datatype New = new_instance CTypeId    ― ‹New object, can only be of a concrete class type› 
             | new_array Arraytype nat ― ‹New array with given size›

text ‹The discriminator isNewArr› can be used to distinguish both 
kinds of newly created elements.
›

definition isNewArr :: "New  bool" where
"isNewArr t = (case t of 
                 new_instance C  False     
               | new_array T l  True)"   

lemma isNewArr_simps [simp]:
"isNewArr (new_instance C) = False"
"isNewArr (new_array T l)  = True"
  by (simp_all add: isNewArr_def)

text ‹The function typeofNew› yields the type of the newly created
element.›

definition typeofNew :: "New  Javatype" where
"typeofNew n = (case n of
                  new_instance C  CClassT C
                | new_array T l   ArrT T)"

lemma typeofNew_simps:
"typeofNew (new_instance C) = CClassT C"
"typeofNew (new_array T l)  = ArrT T"
  by (simp_all add: typeofNew_def)

subsection ‹The Definition of the Store›

text ‹In our store model, all objects\footnote{In the following, the term ``objects'' 
includes arrays. This keeps the explanations compact.}
of all classes exist at all times, but only those objects that have already been allocated
are alive. Objects cannot be deallocated, thus an object that once gained
the aliveness status cannot lose it later on.
\\[12pt]
 To model the store, we need two functions that give us fresh object Id's for 
the allocation of new objects (function newOID›) and arrays
(function newAID›) as well as a function that maps locations to
their contents (function vals›).›

record StoreImpl = newOID :: "CTypeId  ObjectId"
                   newAID :: "Arraytype  ObjectId"
                   vals   :: "Location  Value"

text ‹The function aliveImpl› determines for a given value whether
it is alive in a given store.
›

definition aliveImpl::"Value  StoreImpl  bool" where
"aliveImpl x s = (case x of
                    boolV b   True
                  | intgV i   True
                  | shortV s   True
                  | byteV by   True
                  | objV C a  (a < newOID s C)
                  | arrV T a  (a < newAID s T)
                  | nullV     True)"


text ‹The store itself is defined as new type. The store ensures
and maintains the following 
properties: All stored values are alive; for all locations whose values are
not alive, the store yields the location type's init value; and
all stored values are of the correct type (i.e.~of the type of the location
they are stored in).
›

definition "Store = {s. ( l. aliveImpl (vals s l) s)  
                  ( l. ¬ aliveImpl (ref l) s  vals s l = init (ltype l)) 
                  ( l. typeof (vals s l)  ltype l)}"

typedef Store = Store
  unfolding Store_def
  apply (rule exI [where ?x=" newOID = (λC. 0),
                          newAID = (λT. 0),
                          vals = (λl. init (ltype l)) "])
  apply (auto simp add: aliveImpl_def init_def NullT_leaf_array split: Javatype.splits)
  done

text ‹One might also model the Store as axiomatic type class and prove that the type StoreImpl belongs
to this type class. This way, a clearer separation between the axiomatic description of the store and its
properties on the one hand and the realization that has been chosen in this formalization on the other hand
could be achieved. Additionally, it would be easier to make use of  different store implementations that
might have different additional features. This separation remains to be performed as future work.
›

subsection‹The Store Interface›

text ‹The Store interface consists of five functions:
access› to read the value that is stored at a location;
alive› to test whether a value is alive in the store;
alloc› to allocate a new element in the store;
new› to read the value of a newly allocated element;
update› to change the value that is stored at a location.
›

consts access:: "Store  Location  Value"  ("_@@_" [71,71] 70)     
       alive:: "Value  Store  bool"
       alloc:: "Store  New  Store" 
       new:: "Store  New  Value"
       update:: "Store  Location  Value  Store"
       
nonterminal smodifybinds and smodifybind
syntax
  "_smodifybind" :: "['a, 'a]      smodifybind" ("(2_ :=/ _)")
  ""         :: "smodifybind  smodifybinds"     ("_")
  ""         :: "CTypeId  smodifybind"          ("_")
  "_smodifybinds":: "[smodifybind, smodifybinds] => smodifybinds" ("_,/ _")
  "_sModify"  :: "['a, smodifybinds]  'a"       ("_/(_)" [900,0] 900)
translations
  "_sModify s (_smodifybinds b bs)"  == "_sModify (_sModify s b) bs"
  "sx:=y"                          == "CONST update s x y"
  "sc"                             == "CONST alloc s c" 
 

text ‹With this syntactic setup we can write chains of (array) updates and 
allocations like in the
following term  
@{term "snew_instance Node,x:=y,z:=intgV 3,new_array IntgAT 3,a.[i]:=intgV 4,k:=boolV True"}. 
›

text ‹In the following, the definitions of the five store interface functions and some lemmas 
about them are given.›

overloading alive  alive
begin
  definition alive where "alive x s  aliveImpl x (Rep_Store s)"
end

lemma alive_trivial_simps [simp,intro]:
"alive (boolV b) s"
"alive (intgV i) s"
"alive (shortV sh) s"
"alive (byteV by) s"
"alive nullV     s"
  by (simp_all add: alive_def aliveImpl_def)

overloading
  access  access
  update  update
  alloc  alloc
  new  new
begin

definition access
  where "access s l  vals (Rep_Store s) l"

definition update
  where "update s l v 
    if alive (ref l) s  alive v s  typeof v  ltype l 
    then Abs_Store ((Rep_Store s)vals:=(vals (Rep_Store s))(l:=v))
    else s"

definition alloc
  where "alloc s t 
    (case t of 
       new_instance C 
         Abs_Store 
            ((Rep_Store s)newOID := λ D. if C=D 
                              then Suc (newOID (Rep_Store s) C) 
                              else newOID (Rep_Store s) D)
     | new_array T l
         Abs_Store
            ((Rep_Store s)newAID := λ S. if T=S 
                             then Suc (newAID (Rep_Store s) T)
                             else newAID (Rep_Store s) S,
                           vals :=  (vals (Rep_Store s))
                                      (arrLenLoc T (newAID (Rep_Store s) T) 
                                        := intgV (int l))))"

definition new
  where "new s t 
    (case t of
      new_instance C  objV C (newOID (Rep_Store s) C)
    | new_array T l   arrV T (newAID (Rep_Store s) T))"

end

text ‹The predicate wts› tests whether the store is well-typed.›

definition
wts :: "Store  bool" where
"wts OS = ( (l::Location) . (typeof (OS@@l))  (ltype l))"


subsection ‹Derived Properties of the Store›

text ‹In this subsection, a number of lemmas formalize various properties of the Store.
Especially the 13 axioms are proven that must hold for a modelling of a Store 
(see \cite[p. 45]{Poetzsch-Heffter97specification}). They are labeled with
Store1 to Store13.›

lemma alive_init [simp,intro]: "alive (init T) s"
  by (cases T) (simp_all add: alive_def aliveImpl_def) 

lemma alive_loc [simp]: 
  "isObjV x; typeof x  dtype f  alive (ref (x..f)) s = alive x s"
  by (cases x) (simp_all)

lemma alive_arr_loc [simp]: 
  "isArrV x  alive (ref (x.[i])) s = alive x s"
  by (cases x) (simp_all)

lemma alive_arr_len [simp]: 
  "isArrV x  alive (ref (arr_len x)) s = alive x s"
  by (cases x) (simp_all)

lemma ref_arr_len_new [simp]: 
  "ref (arr_len (new s (new_array T n))) = new s (new_array T n)"
  by (simp add: new_def)

lemma ref_arr_loc_new [simp]: 
  "ref ((new s (new_array T n)).[i]) = new s (new_array T n)"
  by (simp add: new_def)

lemma ref_loc_new [simp]: "CClassT C  dtype f 
   ref ((new s (new_instance C))..f) = new s (new_instance C)"
  by (simp add: new_def)

lemma access_type_safe [simp,intro]: "typeof (s@@l)  ltype l" 
proof -
  have "Rep_Store s  Store"    
    by (rule Rep_Store)
  thus ?thesis
    by (auto simp add: access_def Store_def)
qed

text ‹The store is well-typed by construction.›
lemma always_welltyped_store: "wts OS"
  by (simp add: wts_def access_type_safe)


text ‹Store8›
lemma alive_access [simp,intro]: "alive (s@@l) s"
proof -
  have "Rep_Store s  Store"
    by (rule Rep_Store)
  thus ?thesis
    by (auto simp add: access_def Store_def alive_def aliveImpl_def)
qed

text ‹Store3›
lemma access_unalive [simp]: 
  assumes unalive: "¬ alive (ref l) s" 
  shows "s@@l = init (ltype l)"
proof -
  have "Rep_Store s  Store"
    by (rule Rep_Store)
  with unalive show ?thesis
    by (simp add: access_def Store_def alive_def aliveImpl_def)
qed


lemma update_induct:
  assumes skip: "P s"
  assumes update: "alive (ref l) s; alive v s; typeof v  ltype l 
               P (Abs_Store ((Rep_Store s)vals:=(vals (Rep_Store s))(l:=v)))" 
  shows "P (sl:=v)"
  using update skip 
  by (simp add: update_def)

lemma vals_update_in_Store:
  assumes alive_l: "alive (ref l) s" 
  assumes alive_y: "alive y s" 
  assumes type_conform: "typeof y  ltype l"
  shows "(Rep_Store svals := (vals (Rep_Store s))(l := y))  Store" 
  (is "?s_upd  Store")
proof -
  have s: "Rep_Store s  Store"
    by (rule Rep_Store)
  have alloc_eq: "newOID ?s_upd = newOID (Rep_Store s)"
    by simp
  have " l. aliveImpl (vals ?s_upd l) ?s_upd"
  proof 
    fix k
    show "aliveImpl (vals ?s_upd k) ?s_upd"
    proof (cases "k=l")
      case True
      with alive_y show ?thesis
        by (simp add: alloc_eq alive_def aliveImpl_def split: Value.splits)
    next
      case False
      from s have " l. aliveImpl (vals (Rep_Store s) l) (Rep_Store s)"
        by (simp add: Store_def)
      with False show ?thesis
        by (simp add: aliveImpl_def split: Value.splits)
    qed
  qed
  moreover
  have " l. ¬ aliveImpl (ref l) ?s_upd  vals ?s_upd l = init (ltype l)"
  proof (intro allI impI)
    fix k
    assume unalive: "¬ aliveImpl (ref k) ?s_upd"
    show "vals ?s_upd k = init (ltype k)"
    proof -
      from unalive alive_l
      have "kl"
        by (auto simp add: alive_def aliveImpl_def split: Value.splits)
      hence "vals ?s_upd k = vals (Rep_Store s) k"
        by simp
      moreover from unalive 
      have "¬ aliveImpl (ref k) (Rep_Store s)"
        by (simp add: aliveImpl_def split: Value.splits)
      ultimately show ?thesis
        using s by (simp add: Store_def)
    qed
  qed
  moreover
  have " l. typeof (vals ?s_upd l)  ltype l"
  proof
    fix k show "typeof (vals ?s_upd k)  ltype k"
    proof (cases "k=l")
      case True
      with type_conform show ?thesis
        by simp
    next
      case False
      hence "vals ?s_upd k = vals (Rep_Store s) k"
        by simp
      with s show ?thesis
        by (simp add: Store_def)
    qed
  qed
  ultimately show ?thesis
    by (simp add: Store_def)
qed

text ‹Store6›
lemma alive_update_invariant [simp]: "alive x (sl:=y) = alive x s"
proof (rule update_induct)
  show "alive x s = alive x s"..
next
  assume "alive (ref l) s" "alive y s" "typeof y  ltype l"
  hence "Rep_Store 
          (Abs_Store (Rep_Store svals := (vals (Rep_Store s))(l := y)))
         = Rep_Store svals := (vals (Rep_Store s))(l := y)"
    by (rule vals_update_in_Store [THEN Abs_Store_inverse])
  thus "alive x
         (Abs_Store (Rep_Store svals := (vals (Rep_Store s))(l := y))) =
        alive x s"
    by (simp add: alive_def aliveImpl_def split: Value.split)
qed

text ‹Store1›
lemma access_update_other [simp]: 
  assumes neq_l_m: "l  m" 
  shows "sl:=x@@m = s@@m"
proof (rule update_induct)
  show "s@@m = s@@m" ..
next
  assume "alive (ref l) s" "alive x s" "typeof x  ltype l"
  hence "Rep_Store 
          (Abs_Store (Rep_Store svals := (vals (Rep_Store s))(l := x)))
         = Rep_Store svals := (vals (Rep_Store s))(l := x)"
    by (rule vals_update_in_Store [THEN Abs_Store_inverse])
  with neq_l_m 
  show "Abs_Store (Rep_Store svals := (vals (Rep_Store s))(l := x))@@m = s@@m"
    by (auto simp add: access_def)
qed

text ‹Store2›
lemma update_access_same [simp]: 
  assumes alive_l: "alive (ref l) s" 
  assumes alive_x: "alive x s" 
  assumes widen_x_l: "typeof x  ltype l"
  shows "sl:=x@@l = x"
proof -
  from alive_l alive_x widen_x_l
  have "Rep_Store 
          (Abs_Store (Rep_Store svals := (vals (Rep_Store s))(l := x)))
         = Rep_Store svals := (vals (Rep_Store s))(l := x)"
    by (rule vals_update_in_Store [THEN Abs_Store_inverse])
  hence "Abs_Store (Rep_Store svals := (vals (Rep_Store s))(l := x))@@l = x"
    by (simp add: access_def)
  with alive_l alive_x widen_x_l 
  show ?thesis
    by (simp add: update_def)
qed

text ‹Store4›
lemma update_unalive_val [simp,intro]: "¬ alive x s  sl:=x = s"
  by (simp add: update_def)

lemma update_unalive_loc [simp,intro]: "¬ alive (ref l) s  sl:=x = s"
  by (simp add: update_def)

lemma update_type_mismatch [simp,intro]: "¬ typeof x  ltype l  sl:=x = s"
  by (simp add: update_def)


text ‹Store9›
lemma alive_primitive [simp,intro]: "isprimitive (typeof x)  alive x s"
  by (cases x) (simp_all)

text ‹Store10›
lemma new_unalive_old_Store [simp]: "¬ alive (new s t) s"
  by (cases t) (simp_all add: alive_def aliveImpl_def new_def)

lemma alloc_new_instance_in_Store:
"(Rep_Store snewOID := λD. if C = D
                                   then Suc (newOID (Rep_Store s) C)
                                   else newOID (Rep_Store s) D)  Store"
(is "?s_alloc  Store")
proof -
  have s: "Rep_Store s  Store"
    by (rule Rep_Store)
  hence " l. aliveImpl (vals (Rep_Store s) l) (Rep_Store s)"
    by (simp add: Store_def)
  then
  have " l. aliveImpl (vals ?s_alloc l) ?s_alloc"
    by (auto intro: less_SucI simp add: aliveImpl_def split: Value.splits)
  moreover
  have " l. ¬ aliveImpl (ref l) ?s_alloc  vals ?s_alloc l = init (ltype l)"
  proof (intro allI impI)
    fix l
    assume "¬ aliveImpl (ref l) ?s_alloc"
    hence "¬ aliveImpl (ref l) (Rep_Store s)"
      by (simp add: aliveImpl_def split: Value.splits if_split_asm)
    with s have "vals (Rep_Store s) l = init (ltype l)"
      by (simp add: Store_def)
    thus "vals ?s_alloc l = init (ltype l)"
      by simp
  qed
  moreover 
  from s have " l. typeof (vals ?s_alloc l)  ltype l"
    by (simp add: Store_def)
  ultimately
  show ?thesis
    by (simp add: Store_def)
qed

lemma alloc_new_array_in_Store:
"(Rep_Store s newAID :=
                  λS. if T = S
                      then Suc (newAID (Rep_Store s) T)
                      else newAID (Rep_Store s) S,
               vals := (vals (Rep_Store s))
                         (arrLenLoc T
                           (newAID (Rep_Store s) T) :=
                           intgV (int n)))  Store"
(is "?s_alloc  Store")
proof -
  have s: "Rep_Store s  Store"
    by (rule Rep_Store)
  have " l. aliveImpl (vals ?s_alloc l) ?s_alloc"
  proof 
    fix l show "aliveImpl (vals ?s_alloc l) ?s_alloc"
    proof (cases "l = arrLenLoc T (newAID (Rep_Store s) T)")
      case True
      thus ?thesis
        by (simp add: aliveImpl_def split: Value.splits)
    next
      case False
      from s have " l. aliveImpl (vals (Rep_Store s) l) (Rep_Store s)"
        by (simp add: Store_def)
      with False show ?thesis
        by (auto intro: less_SucI simp add: aliveImpl_def split: Value.splits)
    qed
  qed
  moreover
  have " l. ¬ aliveImpl (ref l) ?s_alloc  vals ?s_alloc l = init (ltype l)"
  proof (intro allI impI)
    fix l
    assume unalive: "¬ aliveImpl (ref l) ?s_alloc"
    show "vals ?s_alloc l = init (ltype l)"
    proof (cases "l = arrLenLoc T (newAID (Rep_Store s) T)")
      case True
      with unalive show ?thesis by (simp add: aliveImpl_def)
    next
      case False
      from unalive
      have "¬ aliveImpl (ref l) (Rep_Store s)"
        by (simp add: aliveImpl_def split: Value.splits if_split_asm)
      with s have "vals (Rep_Store s) l = init (ltype l)"
        by (simp add: Store_def)
      with False show ?thesis 
        by simp
    qed
  qed
  moreover 
  from s have " l. typeof (vals ?s_alloc l)  ltype l"
    by (simp add: Store_def)
  ultimately
  show ?thesis
    by (simp add: Store_def)
qed


lemma new_alive_alloc [simp,intro]: "alive (new s t) (st)"
proof (cases t)
  case new_instance thus ?thesis 
    by (simp add: alive_def aliveImpl_def new_def alloc_def
                  alloc_new_instance_in_Store [THEN Abs_Store_inverse])
next
  case new_array thus ?thesis
    by (simp add: alive_def aliveImpl_def new_def alloc_def
                  alloc_new_array_in_Store [THEN Abs_Store_inverse])
qed
 
lemma value_class_inhabitants: 
"(x. typeof x = CClassT typeId  P x) = ( a. P (objV typeId a))"
  (is "( x. ?A x) = ?B")
proof 
  assume " x. ?A x" thus "?B"
    by simp
next
  assume B: "?B" show " x. ?A x"
  proof
    fix x from B show "?A x"
      by (cases x) auto
  qed
qed
   
lemma value_array_inhabitants: 
"(x. typeof x = ArrT typeId  P x) = ( a. P (arrV typeId a))"
  (is "( x. ?A x) = ?B")
proof 
  assume " x. ?A x" thus "?B"
    by simp
next
  assume B: "?B" show " x. ?A x"
  proof
    fix x from B show "?A x"
      by (cases x) auto
  qed
qed


text ‹The following three lemmas are helper lemmas that are not related to the store theory.
They might as well be stored in a separate helper theory.
›

lemma le_Suc_eq: "(a. (a < Suc n) = (a < Suc m)) = (a. (a < n) = (a < m))"
 (is "(a. ?A a) = ( a. ?B a)")
proof
  assume "a. ?A a" thus " a. ?B a"
    by fastforce
next
  assume B: " a. ?B a"
  show "a. ?A a"
  proof
    fix a 
    from B show "?A a"
      by (cases a) simp_all
  qed
qed

lemma all_le_eq_imp_eq: " c::nat. (a. (a < d) = (a < c))  (d = c)" 
proof (induct d)
  case 0 thus ?case by fastforce
next
  case (Suc n c)
  thus ?case
    by (cases c) (auto simp add: le_Suc_eq)
qed
 
lemma all_le_eq: "( a::nat. (a < d) = (a < c)) = (d = c)"
using all_le_eq_imp_eq by auto

text ‹Store11›
lemma typeof_new: "typeof (new s t) = typeofNew t"
  by (cases t) (simp_all add: new_def typeofNew_def)

text ‹Store12›
lemma new_eq: "(new s1 t = new s2 t) = 
                 ( x. typeof x = typeofNew t  alive x s1 = alive x s2)"
by (cases t)
   (auto simp add: new_def typeofNew_def alive_def aliveImpl_def
                   value_class_inhabitants value_array_inhabitants all_le_eq)

lemma new_update [simp]: "new (sl:=x) t = new s t"
  by (simp add: new_eq)

lemma alive_alloc_propagation: 
  assumes alive_s: "alive x s" shows  "alive x (st)"
proof (cases t)
  case new_instance with alive_s show ?thesis
    by (cases x) 
       (simp_all add: alive_def aliveImpl_def alloc_def 
                      alloc_new_instance_in_Store [THEN Abs_Store_inverse])
next
  case new_array with alive_s show ?thesis
    by (cases x) 
       (simp_all add: alive_def aliveImpl_def alloc_def 
                      alloc_new_array_in_Store [THEN Abs_Store_inverse])
qed
  
text ‹Store7› 
lemma alive_alloc_exhaust: "alive x (st) = (alive x s  (x = new s t))"
proof 
  assume alive_alloc: "alive x (st)"
  show "alive x s  x = new s t"
  proof (cases t)
    case (new_instance C) 
    with alive_alloc show ?thesis 
      by (cases x) (auto split: if_split_asm 
                         simp add: alive_def new_def alloc_def aliveImpl_def
                              alloc_new_instance_in_Store [THEN Abs_Store_inverse])
  next
    case (new_array T l)
    with alive_alloc show ?thesis
      by (cases x) (auto split: if_split_asm
                         simp add: alive_def new_def alloc_def aliveImpl_def
                         alloc_new_array_in_Store [THEN Abs_Store_inverse])
  qed
next
  assume "alive x s  x = new s t"
  then show "alive x (st)"
  proof 
    assume "alive x s" thus ?thesis by (rule alive_alloc_propagation)
  next
    assume new: "x=new s t" show ?thesis 
    proof (cases t)
      case new_instance with new show ?thesis
        by (simp add: alive_def aliveImpl_def new_def alloc_def
                      alloc_new_instance_in_Store [THEN Abs_Store_inverse])
    next
      case new_array with new show ?thesis
        by (simp add: alive_def aliveImpl_def new_def alloc_def
                      alloc_new_array_in_Store [THEN Abs_Store_inverse])
    qed
  qed
qed

lemma alive_alloc_cases [consumes 1]: 
  "alive x (st); alive x s  P; x=new s t  P
    P"
  by (auto simp add: alive_alloc_exhaust)

lemma aliveImpl_vals_independent: "aliveImpl x (svals := z) = aliveImpl x s"
  by (cases x) (simp_all add: aliveImpl_def)

lemma access_arr_len_new_alloc [simp]: 
  "snew_array T l@@arr_len (new s (new_array T l)) = intgV (int l)"
  by (subst access_def) 
     (simp add: new_def alloc_def alive_def 
                alloc_new_array_in_Store [THEN Abs_Store_inverse] access_def)

lemma access_new [simp]:
  assumes ref_new: "ref l = new s t"
  assumes no_arr_len: "isNewArr t  l  arr_len (new s t)"
  shows "st@@l = init (ltype l)"
proof -
  from ref_new 
  have "¬ alive (ref l) s"
    by simp
  hence "s@@l = init (ltype l)"
    by simp
  moreover
  from ref_new
  have "alive (ref l) (st)"
    by simp
  moreover
  from no_arr_len
  have "vals (Rep_Store (st)) l = s@@l"
    by (cases t)
       (simp_all add: alloc_def new_def access_def
                  alloc_new_instance_in_Store [THEN Abs_Store_inverse] 
                  alloc_new_array_in_Store [THEN Abs_Store_inverse] )
  ultimately show "st@@l = init (ltype l)"
    by (subst access_def) (simp)
qed

text ‹Store5. We have to take into account that the length of an array
is changed during allocation.›
lemma access_alloc [simp]:
  assumes no_arr_len_new: "isNewArr t  l  arr_len (new s t)"
  shows "st@@l = s@@l"
proof -
  show ?thesis
  proof (cases "alive (ref l) (st)")
    case True
    then
    have access_alloc_vals: "st@@l = vals (Rep_Store (st)) l"
      by (simp add: access_def alloc_def)
    from True show ?thesis
    proof (cases rule: alive_alloc_cases)
      assume alive_l_s: "alive (ref l) s"
      with new_unalive_old_Store
      have l_not_new: "ref l  new s t"
        by fastforce
      hence "vals (Rep_Store (st)) l = s@@l"
        by (cases t) 
           (auto simp add: alloc_def new_def access_def 
                 alloc_new_instance_in_Store [THEN Abs_Store_inverse] 
                 alloc_new_array_in_Store [THEN Abs_Store_inverse])
      with access_alloc_vals 
      show ?thesis 
        by simp
    next
      assume ref_new: "ref l = new s t"
      with no_arr_len_new
      have "st@@l = init (ltype l)"
        by (simp add: access_new)
      moreover
      from ref_new have "s@@l = init (ltype l)"
        by simp
      ultimately
      show ?thesis by simp
    qed
  next
    case False
    hence "st@@l = init (ltype l)"
      by (simp)
    moreover
    from False have "¬ alive (ref l) s"
      by (auto simp add: alive_alloc_propagation)
    hence "s@@l = init (ltype l)"
      by simp
    ultimately show ?thesis by simp
  qed
qed
   
text ‹Store13›
lemma Store_eqI: 
  assumes eq_alive: " x. alive x s1 = alive x s2" 
  assumes eq_access: " l. s1@@l = s2@@l"
  shows "s1=s2"
proof (cases "s1=s2")
  case True thus ?thesis .
next
  case False note neq_s1_s2 = this
  show ?thesis
  proof (cases "newOID (Rep_Store s1) = newOID (Rep_Store s2)")
    case False
    have " C. newOID (Rep_Store s1) C  newOID (Rep_Store s2) C"
    proof (rule ccontr)
      assume "¬ (C. newOID (Rep_Store s1) C  newOID (Rep_Store s2) C)"
      then have "newOID (Rep_Store s1) = newOID (Rep_Store s2)"
        by (blast intro: ext)
      with False show False ..
    qed
    with eq_alive obtain C 
      where "newOID (Rep_Store s1) C  newOID (Rep_Store s2) C"
            " a. alive (objV C a) s1 = alive (objV C a) s2" by auto
    then show ?thesis
      by (simp add: all_le_eq alive_def aliveImpl_def)
  next
    case True note eq_newOID = this
    show ?thesis
    proof (cases "newAID (Rep_Store s1) = newAID (Rep_Store s2)")
      case False
      have " T. newAID (Rep_Store s1) T  newAID (Rep_Store s2) T"
      proof (rule ccontr)
        assume "¬ (T. newAID (Rep_Store s1) T  newAID (Rep_Store s2) T)"
        then have "newAID (Rep_Store s1) = newAID (Rep_Store s2)"
          by (blast intro: ext)
        with False show False ..
      qed
      with eq_alive obtain T 
        where "newAID (Rep_Store s1) T  newAID (Rep_Store s2) T"
              " a. alive (arrV T a) s1 = alive (arrV T a) s2" by auto
      then show ?thesis
        by (simp add: all_le_eq alive_def aliveImpl_def)
    next
      case True note eq_newAID = this
      show ?thesis
      proof (cases "vals (Rep_Store s1) = vals (Rep_Store s2)")
        case True
        with eq_newOID eq_newAID 
        have "(Rep_Store s1) = (Rep_Store s2)"
          by (cases "Rep_Store s1",cases "Rep_Store s2") simp
        hence "s1=s2"
          by (simp add: Rep_Store_inject)
        with neq_s1_s2 show ?thesis
          by simp
      next
        case False
        have " l. vals (Rep_Store s1) l  vals (Rep_Store s2) l"
        proof (rule ccontr)
          assume "¬ (l. vals (Rep_Store s1) l  vals (Rep_Store s2) l)"
          hence "vals (Rep_Store s1) = vals (Rep_Store s2)"
            by (blast intro: ext)
          with False show False ..
        qed
        then obtain l
          where "vals (Rep_Store s1) l  vals (Rep_Store s2) l"
          by auto
        with eq_access have "False"
          by (simp add: access_def)
        thus ?thesis ..
      qed
    qed
  qed
qed

text ‹Lemma 3.1 in [Poetzsch-Heffter97]. The proof of this lemma is quite an
impressive demostration of readable Isar proofs since it closely follows the
textual proof.›
lemma comm: 
  assumes neq_l_new: "ref l  new s t"
  assumes neq_x_new: "x  new s t"
  shows "stl:=x = sl:=xt"
proof (rule Store_eqI [rule_format])
  fix y
  show "alive y (stl:=x) = alive y (sl:=xt)"                          
  proof -
    have "alive y (stl:=x) = alive y (st)"
      by (rule alive_update_invariant)
    also have " = (alive y s  (y = new s t))"
      by (rule alive_alloc_exhaust)
    also have " = (alive y (sl:=x)  y = new s t)"
      by (simp only: alive_update_invariant)
    also have " = (alive y (sl:=x)  y = new (sl:=x) t)"
    proof -
      have "new s t = new (sl:=x) t"
        by simp
      thus ?thesis by simp
    qed
    also have " = alive y (sl:=xt)"
      by (simp add: alive_alloc_exhaust)
    finally show ?thesis .
  qed
next
  fix k
  show "stl := x@@k = sl := xt@@k"
  proof (cases "l=k")
    case False note neq_l_k = this
    show ?thesis
    proof (cases "isNewArr t  k  arr_len (new s t)")
      case True
      from neq_l_k 
      have  "stl := x@@k = st@@k" by simp
      also from True 
      have " = s@@k" by simp
      also from neq_l_k 
      have " = sl:=x@@k" by simp
      also from True
      have " = sl := xt@@k"  by simp
      finally show ?thesis .
    next
      case False
      then obtain T n where 
        t: "t=new_array T n" and k: "k=arr_len (new s (new_array T n))"
        by (cases t) auto
      from k have k': "k=arr_len (new (sl := x) (new_array T n))"
        by simp
      from neq_l_k 
      have  "stl := x@@k = st@@k" by simp
      also from t k 
      have " = intgV (int n)"
        by simp
      also from t k'
      have " = sl := xt@@k"
        by (simp del: new_update)
      finally show ?thesis .
    qed
  next
    case True note eq_l_k = this
    have lemma_3_1: 
      "ref l  new s t  alive (ref l) (st) = alive (ref l) s"         
      by (simp add: alive_alloc_exhaust)
    have lemma_3_2: 
      "x  new s t  alive x (st) = alive x s"    
      by (simp add: alive_alloc_exhaust)
    have lemma_3_3: "sl:=x,t@@l = sl:=x@@l"
    proof -
      from neq_l_new have "ref l  new (sl:=x) t"
        by simp
      hence "isNewArr t  l  arr_len (new (sl:=x) t)"
        by (cases t) auto
      thus ?thesis
        by (simp)
    qed
    show ?thesis
    proof (cases "alive x s")
      case True note alive_x = this
      show ?thesis
      proof (cases "alive (ref l) s")
        case True note alive_l = this
        show ?thesis
        proof (cases "typeof x  ltype l")
          case True 
          with alive_l alive_x
          have "sl:=x@@l = x"
            by (rule update_access_same)
          moreover
          have "stl:=x@@l = x"
          proof -
            from alive_l neq_l_new have "alive (ref l) (st)"
              by (simp add: lemma_3_1)
            moreover
            from alive_x neq_x_new have "alive x (st)"
              by (simp add: lemma_3_2)
            ultimately
            show "stl:=x@@l = x"
              using True by (rule update_access_same)
          qed
          ultimately show ?thesis 
            using eq_l_k lemma_3_3 by simp
        next
          case False
          thus ?thesis by simp
        qed
      next
        case False note not_alive_l = this
        from not_alive_l neq_l_new have "¬ alive (ref l) (st)"
          by (simp add: lemma_3_1)
        then have "stl:=x@@l = init (ltype l)"
          by simp
        also from not_alive_l have " = sl:=x@@l"
          by simp
        also have " = sl:=xt@@l" 
          by (simp add: lemma_3_3)
        finally show ?thesis by (simp add: eq_l_k)
      qed
    next
      case False note not_alive_x = this
      from not_alive_x neq_x_new have "¬ alive x (st)"
        by (simp add: lemma_3_2)
      then have "stl:=x@@l = st@@l"
        by (simp)
      also have " = s@@l"
      proof -
        from neq_l_new 
        have "isNewArr t  l  arr_len (new s t)"
          by (cases t) auto
        thus ?thesis
          by (simp)
      qed
      also from not_alive_x have " = sl:=x@@l"
        by (simp)
      also have " = sl:=xt@@l"
        by (simp add: lemma_3_3)
      finally show ?thesis by (simp add: eq_l_k)
    qed
  qed
qed


end 

Theory StoreProperties

(*  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 ‹Store Properties›

theory StoreProperties
imports Store
begin

text ‹This theory formalizes advanced concepts and properties of stores.›

subsection ‹Reachability of a Location from a Reference›

text ‹For a given store, the function reachS› yields the set of all pairs 
$(l,v)$ where $l$ is a location that is reachable from the value $v$ (which must be a reference)
in the given store.
The predicate reach› decides whether a location is reachable from a value in a store.
›

inductive
  reach :: "Store  Location  Value  bool" 
    ("_ _ reachable'_from _" [91,91,91]90)
  for s :: Store
where
  Immediate: "ref l  nullV  s l reachable_from (ref l)"
| Indirect: "s l reachable_from (s@@k); ref k  nullV 
              s l reachable_from (ref k)" 

text ‹Note that we explicitly exclude nullV› as legal reference
for reachability. 
Keep in mind that static fields are not associated to any object,
therefore ref› yields nullV› if invoked on static fields 
(see the
definition of the function ref›, Sect. \ref{ref_def}).
Reachability only describes the locations directly 
reachable from the object or array by following the pointers and should not include 
the static fields if we encounter a nullV› reference in the pointer 
chain.›

text ‹We formalize some properties of reachability. 
Especially, Lemma 3.2 as given in \cite[p. 53]{Poetzsch-Heffter97specification} is proven.›

lemma unreachable_Null: 
  assumes reach: "s l reachable_from x" shows "xnullV"
  using reach by (induct) auto

corollary unreachable_Null_simp [simp]:
  "¬ s l reachable_from nullV"
  by (iprover dest: unreachable_Null)

corollary unreachable_NullE [elim]:
  "s l reachable_from nullV  P"
  by (simp)

lemma reachObjLoc [simp,intro]: 
  "C=cls cf  s objLoc cf a reachable_from objV C a"
  by (iprover intro: reach.Immediate [of "objLoc cf a",simplified])

lemma reachArrLoc [simp,intro]: "s arrLoc T a i reachable_from arrV T a"
  by (rule reach.Immediate [of "arrLoc T a i",simplified])

lemma reachArrLen [simp,intro]: "s arrLenLoc T a reachable_from arrV T a"
  by (rule reach.Immediate [of "arrLenLoc T a",simplified])

lemma unreachStatic [simp]: "¬ s staticLoc f reachable_from x"
proof -
  {
    fix y assume "s y reachable_from x" "y=staticLoc f"
    then have False
      by induct auto
  }
  thus ?thesis
    by auto
qed

lemma unreachStaticE [elim]: "s staticLoc f reachable_from x  P"
  by (simp add: unreachStatic)

lemma reachable_from_ArrLoc_impl_Arr [simp,intro]:
  assumes reach_loc: "s l reachable_from (s@@arrLoc T a i)"
  shows "s l reachable_from (arrV T a)"
  using reach.Indirect [OF reach_loc]
  by simp

lemma reachable_from_ObjLoc_impl_Obj [simp,intro]:
  assumes reach_loc: "s l reachable_from (s@@objLoc cf a)"
  assumes C: "C=cls cf"
  shows "s l reachable_from (objV C a)"
  using C reach.Indirect [OF reach_loc]
  by simp


text ‹Lemma 3.2 (i)›
lemma reach_update [simp]:
  assumes unreachable_l_x: "¬ s l reachable_from x" 
  shows "sl:=y k reachable_from  x = s k reachable_from x"
proof
  assume "s k reachable_from x"
  from this unreachable_l_x
  show "sl := y k reachable_from x"
  proof (induct)
    case (Immediate k)
    have "ref k  nullV" by fact
    then show "sl := y k reachable_from (ref k)"
      by (rule reach.Immediate)
  next
    case (Indirect k m)
    have hyp: "¬ s l reachable_from (s@@m) 
                sl:=y  k reachable_from (s@@m)" by fact
    have "ref m  nullV" and "¬ s l reachable_from (ref m)" by fact+
    hence "lm" "¬ s l reachable_from (s@@m)"
      by (auto intro: reach.intros)
    with hyp have "sl := y  k reachable_from (sl := y@@m)"
      by simp
    then show "sl := y k reachable_from (ref m)"
      by (rule reach.Indirect) (rule Indirect.hyps)
  qed
next
  assume "sl := y k reachable_from x"
  from this unreachable_l_x
  show "s k reachable_from x"
  proof (induct)
    case (Immediate k)
    have "ref k  nullV" by fact
    then show "s  k reachable_from (ref k)"
      by (rule reach.Immediate)
  next
    case (Indirect k m)
    with Indirect.hyps 
    have hyp: "¬ s l reachable_from (sl := y@@m)  
                s k reachable_from (sl := y@@m)" by simp
    have "ref m  nullV" and "¬ s l reachable_from (ref m)" by fact+
    hence "lm" "¬ s  l reachable_from (s@@m)"  
      by (auto intro: reach.intros)
    with hyp have "s  k reachable_from (s@@m)"
      by simp
    thus "s k reachable_from (ref m)"
      by (rule reach.Indirect) (rule Indirect.hyps)
  qed
qed


text ‹Lemma 3.2 (ii)›
lemma reach2: 
  "¬ s l reachable_from x  ¬ sl:=y l reachable_from x"
  by (simp)

text ‹Lemma 3.2 (iv)›
lemma reach4: "¬ s  l reachable_from (ref k)  k  l  (ref k) = nullV"
  by (auto intro: reach.intros)

lemma reachable_isRef: 
  assumes reach: "sl reachable_from x" 
  shows "isRefV x"
  using reach 
proof (induct)
  case (Immediate l)
  show "isRefV (ref l)"
    by (cases l) simp_all
next
  case (Indirect l k)
  show "isRefV (ref k)"
    by (cases k) simp_all
qed


lemma val_ArrLen_IntgT: "isArrLenLoc l  typeof (s@@l) = IntgT"
proof -
  assume isArrLen: "isArrLenLoc l"
  have T: "typeof (s@@l)  ltype l"
    by (simp)
  also from isArrLen have I: "ltype l = IntgT"
    by (cases l) simp_all
  finally show ?thesis
    by (auto elim: rtranclE simp add: le_Javatype_def subtype_defs)
qed

lemma access_alloc' [simp]:
  assumes no_arr_len: "¬ isArrLenLoc l"
  shows "st@@l = s@@l"
proof -
  from no_arr_len 
  have "isNewArr t  l  arr_len (new s t)"
    by (cases t) (auto simp add: new_def isArrLenLoc_def split: Location.splits)
  thus ?thesis 
    by (rule access_alloc)
qed
 
text ‹Lemma 3.2 (v)›
lemma reach_alloc [simp]: "st l reachable_from x = s l reachable_from x"
proof 
  assume "st l reachable_from x"
  thus "s l reachable_from x"
  proof (induct)
    case (Immediate l)
    thus "s l reachable_from ref l"
      by (rule reach.intros)
  next
    case (Indirect l k)
    have reach_k: "s l reachable_from (st@@k)" by fact
    moreover
    have "st@@k = s@@k"
    proof -
      from reach_k have isRef: "isRefV (st@@k)"
        by (rule reachable_isRef)
      have "¬ isArrLenLoc k"
      proof (rule ccontr,simp)
        assume "isArrLenLoc k"
        then have "typeof (st@@k) = IntgT"
          by (rule val_ArrLen_IntgT)
        with isRef 
        show "False"
          by (cases "(st@@k)") simp_all
      qed
      thus ?thesis
        by (rule access_alloc')
    qed
    ultimately have "s l reachable_from (s@@k)"
      by simp
    thus "s l reachable_from ref k"
      by (rule reach.intros) (rule Indirect.hyps)
  qed
next
  assume "s l reachable_from x"
  thus "st l reachable_from x"
  proof (induct)
    case (Immediate l)
    thus "st l reachable_from ref l"
      by (rule reach.intros)
  next
    case (Indirect l k)
    have reach_k: "st l reachable_from (s@@k)" by fact
    moreover
    have "st@@k = s@@k"
    proof -
      from reach_k have isRef: "isRefV (s@@k)"
        by (rule reachable_isRef)
      have "¬ isArrLenLoc k"
      proof (rule ccontr,simp)
        assume "isArrLenLoc k"
        then have "typeof (s@@k) = IntgT"
          by (rule val_ArrLen_IntgT)
        with isRef 
        show "False"
          by (cases "(s@@k)") simp_all
      qed
      thus ?thesis
        by (rule access_alloc')
    qed
    ultimately have "st l reachable_from (st@@k)"
      by simp
    thus "st l reachable_from ref k"
      by (rule reach.intros) (rule Indirect.hyps)
  qed
qed
       

text ‹Lemma 3.2 (vi)›
lemma reach6: "isprimitive(typeof x)  ¬ s  l reachable_from x"
proof 
  assume prim: "isprimitive(typeof x)"
  assume "s  l reachable_from x"
  hence "isRefV x"
    by (rule reachable_isRef)
  with prim show False
    by (cases x) simp_all
qed

text ‹Lemma 3.2 (iii)›
lemma reach3: 
  assumes k_y: "¬ s k reachable_from y"
  assumes k_x: "¬ s k reachable_from x"
  shows "¬ sl:=y k reachable_from x"
proof
  assume "sl:=y k reachable_from x"
  from this k_y k_x
  show False
  proof (induct)
    case (Immediate l)
    have "¬ s l reachable_from ref l" and "ref l  nullV" by fact+
    thus False
      by (iprover intro: reach.intros)
  next
    case (Indirect m k)
    have k_not_Null: "ref k  nullV" by fact
    have not_m_y: "¬ s m reachable_from y" by fact
    have not_m_k: "¬ s m reachable_from ref k" by fact
    have hyp: "¬ s m reachable_from y; ¬ s m reachable_from (sl := y@@k)
                False" by fact
    have m_upd_k: "sl := y m reachable_from (sl := y@@k)" by fact
    show False
    proof (cases "l=k")
      case False
      then have "sl := y@@k = s@@k" by simp
      moreover 
      from not_m_k k_not_Null have "¬ s m reachable_from (s@@k)"
        by (iprover intro: reach.intros)
      ultimately show False
        using not_m_y hyp by simp
    next
      case True note eq_l_k = this
      show ?thesis
      proof (cases "alive (ref l) s  alive y s  typeof y  ltype l")
        case True
        with eq_l_k have "sl := y@@k = y"
          by simp
        with not_m_y hyp show False by simp
      next
        case False
        hence "sl := y = s"
          by auto
        moreover 
        from not_m_k k_not_Null have "¬ s m reachable_from (s@@k)"
          by (iprover intro: reach.intros)
        ultimately show False
          using not_m_y hyp by simp
      qed
    qed
  qed
qed



text ‹Lemma 3.2 (vii).›

lemma unreachable_from_init [simp,intro]: "¬ s l reachable_from (init T)"
  using reach6 by (cases T) simp_all

lemma ref_reach_unalive: 
  assumes unalive_x:"¬ alive x s" 
  assumes l_x: "s l reachable_from x" 
  shows "x = ref l"
using l_x unalive_x
proof induct
  case (Immediate l)
  show "ref l = ref l"
    by simp
next
  case (Indirect l k)
  have "ref k  nullV" by fact
  have "¬ alive (ref k) s" by fact
  hence "s@@k = init (ltype k)" by simp
  moreover have "s l reachable_from (s@@k)" by fact
  ultimately have False by simp
  thus ?case ..
qed

lemma loc_new_reach: 
  assumes l: "ref l = new s t"
  assumes l_x: "s l reachable_from x"
  shows "x = new s t"
using l_x l
proof induct
  case (Immediate l)
  show "ref l = new s t" by fact
next
  case (Indirect l k)
  hence "s@@k = new s t" by iprover
  moreover 
  have "¬ alive (new s t) s"
    by simp
  moreover 
  have "alive (s@@k) s"
    by simp
  ultimately have False by simp
  thus ?case ..
qed
 

text ‹Lemma 3.2 (viii)›
lemma alive_reach_alive: 
  assumes alive_x: "alive x s" 
  assumes reach_l: "s  l reachable_from x" 
  shows "alive (ref l) s"
using reach_l alive_x
proof (induct)
  case (Immediate l)
  show ?case by fact
next
  case (Indirect l k)
  have hyp: "alive (s@@k) s  alive (ref l) s" by fact
  moreover have "alive (s@@k) s" by simp
  ultimately
  show "alive (ref l) s"
    by iprover
qed
 
text ‹Lemma 3.2 (ix)›
lemma reach9: 
  assumes reach_impl_access_eq: "l. s1l reachable_from x  (s1@@l = s2@@l)"
  shows "s1 l reachable_from x = s2 l reachable_from x"
proof 
  assume "s1 l reachable_from x"
  from this reach_impl_access_eq 
  show "s2 l reachable_from x"
  proof (induct)
    case (Immediate l)
    show "s2 l reachable_from ref l"
      by (rule reach.intros) (rule Immediate.hyps)
  next
    case (Indirect l k)
    have hyp: "l. s1 l reachable_from (s1@@k)  s1@@l = s2@@l 
                s2 l reachable_from (s1@@k)" by fact
    have k_not_Null: "ref k  nullV" by fact
    have reach_impl_access_eq: 
      "l. s1 l reachable_from ref k  s1@@l = s2@@l" by fact
    have "s1 l reachable_from (s1@@k)" by fact
    with k_not_Null
    have "s1@@k = s2@@k"
      by (iprover intro: reach_impl_access_eq [rule_format] reach.intros)
    moreover from reach_impl_access_eq k_not_Null
    have "l. s1 l reachable_from (s1@@k)  s1@@l = s2@@l"
      by (iprover intro: reach.intros)
    then have "s2 l reachable_from (s1@@k)"
      by (rule hyp)
    ultimately have "s2 l reachable_from (s2@@k)"
      by simp
    thus "s2 l reachable_from ref k"
      by (rule reach.intros) (rule Indirect.hyps)
  qed
next
  assume "s2 l reachable_from x"
  from this reach_impl_access_eq 
  show "s1 l reachable_from x"
  proof (induct)
    case (Immediate l)
    show "s1 l reachable_from ref l"
      by (rule reach.intros) (rule Immediate.hyps)
  next
    case (Indirect l k)
    have hyp: "l. s1 l reachable_from (s2@@k)  s1@@l = s2@@l 
                s1 l reachable_from (s2@@k)" by fact
    have k_not_Null: "ref k  nullV" by fact
    have reach_impl_access_eq: 
      "l. s1 l reachable_from ref k  s1@@l = s2@@l" by fact
    have "s1 k reachable_from ref k"
      by (rule reach.intros) (rule Indirect.hyps)
    with reach_impl_access_eq
    have eq_k: "s1@@k = s2@@k"
      by simp
    from reach_impl_access_eq k_not_Null
    have "l. s1 l reachable_from (s1@@k)  s1@@l = s2@@l"
      by (iprover intro: reach.intros)
    then 
    have "l. s1 l reachable_from (s2@@k)  s1@@l = s2@@l"
      by (simp add: eq_k)
    with eq_k hyp have "s1 l reachable_from (s1@@k)"
      by simp
    thus "s1 l reachable_from ref k"
      by (rule reach.intros) (rule Indirect.hyps)
   qed
qed


subsection ‹Reachability of a Reference from a Reference›

text ‹The predicate rreach› tests whether a value is reachable from
another value. This is an extension of the predicate oreach› as described
in \cite[p. 54]{Poetzsch-Heffter97specification} because now arrays are handled as well.
›

definition rreach:: "Store  Value  Value  bool" 
  ("_⊢Ref _ reachable'_from _" [91,91,91]90) where
"s⊢Ref y reachable_from x = ( l. s l reachable_from x  y = ref l)"


subsection ‹Disjointness of Reachable Locations›

text ‹The predicate disj› tests whether two values are disjoint
in a given store. Its properties as given in 
\cite[Lemma 3.3, p. 54]{Poetzsch-Heffter97specification} are then proven.
›

definition disj:: "Value  Value  Store  bool" where
"disj x y s = ( l. ¬ s l reachable_from x  ¬ s l reachable_from y)"


lemma disjI1: " l. s l reachable_from x  ¬ s l reachable_from y 
  disj x y s"
  by (simp add: disj_def)

lemma disjI2: " l. s l reachable_from y  ¬ s l reachable_from x 
  disj x y s"
  by (auto simp add: disj_def)

lemma disj_cases [consumes 1]: 
  assumes "disj x y s"
  assumes " l.  ¬ s l reachable_from x  P"
  assumes " l.  ¬ s l reachable_from y  P"
  shows "P"
  using assms by (auto simp add: disj_def)

text ‹Lemma 3.3 (i) in \cite{Poetzsch-Heffter97specification}›
lemma disj1: "disj x y s; ¬ s l reachable_from x; ¬ s l reachable_from y 
               disj x y (sl:=z)"
  by (auto simp add: disj_def)

text ‹Lemma 3.3 (ii)›
lemma disj2: 
  assumes disj_x_y: "disj x y s" 
  assumes disj_x_z: "disj x z s"
  assumes unreach_l_x: "¬ s l reachable_from x"
  shows "disj x y (sl:=z)"
proof (rule disjI1)
  fix k 
  assume reach_k_x: "sl := z k reachable_from x"
  show "¬ sl := z k reachable_from y"
  proof - 
    from unreach_l_x reach_k_x 
    have reach_s_k_x: "s k reachable_from x"
      by simp
    with disj_x_z 
    have "¬ s k reachable_from z"
      by (simp add: disj_def)
    moreover from reach_s_k_x disj_x_y
    have "¬ s k reachable_from y"
      by (simp add: disj_def)
    ultimately show ?thesis
      by (rule reach3)
  qed
qed

   

text ‹Lemma 3.3 (iii)›
lemma disj3: assumes alive_x_s: "alive x s" 
  shows "disj x (new s t) (st)"
proof (rule disjI1,simp only: reach_alloc)
  fix l
  assume reach_l_x: "s l reachable_from x"
  show "¬ s l reachable_from new s t"
  proof 
    assume reach_l_new: "s l reachable_from new s t" 
    have unalive_new: "¬ alive (new s t) s" by simp
    from this reach_l_new
    have  "new s t = ref l"
      by (rule ref_reach_unalive)
    moreover from alive_x_s reach_l_x 
    have "alive (ref l) s"
      by (rule alive_reach_alive)
    ultimately show False
      using unalive_new
      by simp
  qed
qed

text ‹Lemma 3.3 (iv)›
lemma disj4: "disj (objV C a) y s; CClassT C  dtype f   
               disj (s@@(objV C a)..f) y s"
  by (auto simp add: disj_def)
  
lemma disj4': "disj (arrV T a) y s   
               disj (s@@(arrV T a).[i]) y s"
  by (auto simp add: disj_def)


subsection ‹X-Equivalence›

text ‹We call two stores $s_1$ and $s_2$ equivalent wrt. a given value $X$
(which is called X-equivalence)
 iff $X$ and all values
reachable from $X$ in $s_1$ or $s_2$ have the same state \cite[p. 55]{Poetzsch-Heffter97specification}. 
This is tested by  the predicate
xeq›. Lemma 3.4 of  \cite{Poetzsch-Heffter97specification} is then proven for xeq›.
› 

definition xeq:: "Value  Store  Store  bool" where
"xeq x s t = (alive x s = alive x t  
             ( l. s l reachable_from x  s@@l = t@@l))"

abbreviation xeq_syntax :: "Store  Value  Store  bool"
  ("_/ (≡[_])/ _" [900,0,900] 900)
where "s ≡[x] t == xeq x s t"


lemma xeqI: "alive x s = alive x t;  
              l. s l reachable_from x  s@@l = t@@l
               s ≡[x] t"
  by (auto simp add: xeq_def)

text ‹Lemma 3.4 (i) in  \cite{Poetzsch-Heffter97specification}.›
lemma xeq1_refl: "s ≡[x] s"
  by (simp add: xeq_def)

text ‹Lemma 3.4 (i)›
lemma xeq1_sym': 
  assumes s_t: "s ≡[x] t"
  shows "t ≡[x] s"
proof -
  from s_t have "alive x s = alive x t" by (simp add: xeq_def)
  moreover
  from s_t have " l. s l reachable_from x  s@@l = t@@l" 
    by (simp add: xeq_def)
  with reach9 [OF this]
  have " l. t l reachable_from x  t@@l = s@@l" 
    by simp
  ultimately show ?thesis
    by (simp add: xeq_def)
qed
 
lemma xeq1_sym: "s ≡[x] t = t ≡[x] s"
  by (auto intro: xeq1_sym')


text ‹Lemma 3.4 (i)›
lemma xeq1_trans [trans]: 
  assumes s_t: "s ≡[x] t" 
  assumes t_r: "t ≡[x] r" 
  shows "s ≡[x] r"
proof -
  from s_t t_r
  have "alive x s = alive x r"
    by (simp add: xeq_def)
  moreover
  have " l. s l reachable_from x  s@@l = r@@l"
  proof (intro allI impI)
    fix l
    assume reach_l: "s l reachable_from x"
    show "s@@l = r@@l"
    proof -
      from reach_l s_t have "s@@l=t@@l"
        by (simp add: xeq_def)
      also have "t@@l = r@@l"
      proof -
        from s_t have " l. s l reachable_from x  s@@l = t@@l"
          by (simp add: xeq_def)
        from reach9 [OF this] reach_l have "t l reachable_from x"
          by simp
        with t_r show ?thesis
          by (simp add: xeq_def)
      qed
      finally show ?thesis .
    qed
  qed
  ultimately show ?thesis
    by (simp add: xeq_def)
qed
   

  
text ‹Lemma 3.4 (ii)›
lemma xeq2: 
  assumes xeq: " x. s ≡[x] t" 
  assumes static_eq: " f. s@@(staticLoc f) = t@@(staticLoc f)" 
  shows "s = t"
proof (rule Store_eqI)
  from xeq 
  show "x. alive x s = alive x t"
    by (simp add: xeq_def)
next
  show "l. s@@l = t@@l"
  proof 
    fix l 
    show "s@@l = t@@l"
    proof (cases l)
      case (objLoc cf a)
      have "l = objLoc cf a" by fact
      hence "s l reachable_from (objV (cls cf) a)"
        by simp
      with xeq show ?thesis
        by (simp add: xeq_def)
    next
      case (staticLoc f)
      have "l = staticLoc f" by fact
      with static_eq show ?thesis 
        by (simp add: xeq_def)
    next
      case (arrLenLoc T a)
      have "l = arrLenLoc T a" by fact
      hence "s l reachable_from (arrV T a)"
        by simp
      with xeq show ?thesis
        by (simp add: xeq_def)
    next
      case (arrLoc T a i)
      have "l = arrLoc T a i" by fact
      hence "s l reachable_from (arrV T a)"
        by simp
      with xeq show ?thesis
        by (simp add: xeq_def)
    qed
  qed
qed


text ‹Lemma 3.4 (iii)›
lemma xeq3: 
  assumes unreach_l: "¬ s l reachable_from x" 
  shows "s ≡[x] sl:=y"
proof (rule xeqI)
  show "alive x s = alive x (sl := y)"
    by simp
next
  fix k 
  assume reach_k: "s k reachable_from x"
  with unreach_l have "lk" by auto
  then show "s@@k = sl := y@@k"
    by simp
qed



text ‹Lemma 3.4 (iv)›
lemma xeq4: assumes not_new: "x  new s t" 
  shows "s ≡[x] st"
proof (rule xeqI)
  from not_new 
  show "alive x s = alive x (st)"
    by (simp add: alive_alloc_exhaust)
next
  fix l
  assume reach_l: "s l reachable_from x"
  show "s@@l = st@@l"
  proof (cases "isNewArr t  l  arr_len (new s t)")
    case True
    with reach_l show ?thesis
      by simp
  next
    case False
    then obtain T n where t: "t = new_array T n" and
                          l: "l = arr_len (new s t)"
      by (cases t) auto
    hence "ref l = new s t"
      by simp
    from this reach_l
    have "x = new s t"
      by (rule loc_new_reach)
    with not_new show ?thesis ..
  qed
qed

text ‹Lemma 3.4 (v)›
lemma xeq5: "s ≡[x] t  s l reachable_from x = t l reachable_from x"
  by (rule reach9) (simp add:  xeq_def)
  

subsection ‹T-Equivalence›

text ‹T-equivalence is the extension of X-equivalence from values to types. Two stores are
T-equivalent iff they are X-equivalent for all values of type T. This is formalized by the
predicate teq› \cite[p. 55]{Poetzsch-Heffter97specification}.›

definition teq:: "Javatype  Store  Store  bool" where
"teq t s1 s2 = ( x. typeof x  t  s1 ≡[x] s2)"

subsection ‹Less Alive›

text ‹To specify that methods have no side-effects, the following binary relation on stores 
plays a prominent role. It expresses that the two stores differ only in values that are alive
in the store passed as first argument. This is formalized by the predicate lessalive›
\cite[p. 55]{Poetzsch-Heffter97specification}.
The stores have to be X-equivalent for the references of the
first store that are alive, and the values of the static fields have to be the same in both stores.
›

definition lessalive:: "Store  Store  bool" ("_/  _" [70,71] 70)
  where "lessalive s t = (( x. alive x s  s ≡[x] t)  ( f. s@@staticLoc f = t@@staticLoc f))"

text ‹We define an introduction rule for the new operator.›

lemma lessaliveI: 
  " x. alive x s   s ≡[x] t;  f. s@@staticLoc f = t@@staticLoc f
    s  t"
by (simp add: lessalive_def)

text ‹It can be shown that lessalive› is reflexive, transitive and antisymmetric.›

lemma lessalive_refl: "s  s"
  by (simp add: lessalive_def xeq1_refl)

lemma lessalive_trans [trans]: 
  assumes s_t: "s  t"
  assumes t_w: "t  w"
  shows "s  w"
proof (rule lessaliveI)
  fix x 
  assume alive_x_s: "alive x s"
  with s_t have "s ≡[x] t"
    by (simp add: lessalive_def)
  also
  have "t ≡[x] w"
  proof -
    from alive_x_s s_t have "alive x t" by (simp add: lessalive_def xeq_def)
    with t_w show ?thesis
      by (simp add: lessalive_def)
  qed
  finally show "s ≡[x] w".
next
  fix f
  from s_t t_w show "s@@staticLoc f = w@@staticLoc f"
    by (simp add: lessalive_def)
qed

lemma lessalive_antisym:
  assumes s_t: "s  t"
  assumes t_s: "t  s"
  shows "s = t"
proof (rule xeq2)
  show "x. s ≡[x] t"
  proof 
    fix x show "s ≡[x] t"
    proof (cases "alive x s")
      case True
      with s_t show ?thesis by (simp add: lessalive_def)
    next
      case False note unalive_x_s = this
      show ?thesis
      proof (cases "alive x t")
        case True
        with t_s show ?thesis 
          by (subst xeq1_sym) (simp add: lessalive_def)
      next
        case False 
        show ?thesis
        proof (rule xeqI)
          from False unalive_x_s show "alive x s = alive x t" by simp
        next
          fix l assume reach_s_x: "s l reachable_from x"
          with unalive_x_s have x: "x = ref l" 
            by (rule ref_reach_unalive)
          with unalive_x_s have "s@@l = init (ltype l)"
            by simp
          also from reach_s_x x have "t l reachable_from x"
            by (auto intro: reach.Immediate unreachable_Null)
          with False x have "t@@l = init (ltype l)"
            by simp
          finally show "s@@l = t@@l"
            by simp
        qed
      qed
    qed
  qed
next
  from s_t show "f. s@@staticLoc f = t@@staticLoc f"
    by (simp add: lessalive_def)
qed

text ‹This gives us a partial ordering on the store. Thus, the type @{typ "Store"}
can be added to the appropriate type class @{term "ord"} which lets us define the $<$ and
$\leq$ symbols, and to the type class  @{term "order"} which axiomatizes partial orderings.
›

instantiation Store :: order
begin

definition
  le_Store_def: "s  t  s  t"

definition
  less_Store_def: "(s::Store) < t  s  t  ¬ t  s"

text ‹We prove Lemma 3.5 of \cite[p. 56]{Poetzsch-Heffter97specification} for this relation.
›

text ‹Lemma 3.5 (i)›

instance  proof 
  fix s t w:: "Store"
  {
    show "s  s"
      by (simp add: le_Store_def lessalive_refl)
  next
    assume "s  t" "t  w"
    then show "s  w"
      by (unfold le_Store_def) (rule lessalive_trans) 
  next
    assume "s  t" "t  s" 
    then show "s = t"
      by (unfold le_Store_def) (rule lessalive_antisym) 
  next
    show "(s < t) = (s  t  ¬ t  s)"
      by (simp add: less_Store_def)
  }
qed

end

text ‹Lemma 3.5 (ii)›
lemma lessalive2: "s  t; alive x s  alive x t"
  by (simp add: lessalive_def xeq_def)
  

text ‹Lemma 3.5 (iii)›
lemma lessalive3: 
  assumes s_t: "s  t" 
  assumes alive: "alive x s  ¬ alive x t"
  shows "s ≡[x] t"
proof (cases "alive x s")
  case True
  with s_t show ?thesis
    by (simp add: lessalive_def)
next
  case False
  note unalive_x_s = this
  with alive have unalive_x_t: "¬ alive x t"
    by simp
  show ?thesis
  proof (rule xeqI)
    from False alive show "alive x s = alive x t"
      by simp
  next
    fix l assume reach_s_x: "s l reachable_from x"
    with unalive_x_s have x: "x = ref l" 
      by (rule ref_reach_unalive)
    with unalive_x_s have "s@@l = init (ltype l)"
      by simp
    also from reach_s_x x have "t l reachable_from x"
      by (auto intro: reach.Immediate unreachable_Null)
    with unalive_x_t x have "t@@l = init (ltype l)"
      by simp
    finally show "s@@l = t@@l"
      by simp
  qed
qed
   
text ‹Lemma 3.5 (iv)›
lemma lessalive_update [simp,intro]: 
  assumes s_t: "s  t" 
  assumes unalive_l: "¬ alive (ref l) t"
  shows "s  tl:=x"
proof -
  from unalive_l have "tl:=x = t"
    by simp
  with s_t show ?thesis by simp
qed

lemma Xequ4':  
  assumes alive: "alive x s" 
  shows "s ≡[x] st"
proof -
  from alive have "x  new s t"
    by auto
  thus ?thesis
    by (rule xeq4)
qed

  

text ‹Lemma 3.5 (v)›
lemma lessalive_alloc [simp,intro]: "s  st"
  by (simp add: lessalive_def Xequ4')
 

subsection ‹Reachability of Types from Types›

text ‹The predicate treach› denotes the fact that the first type reaches 
the second type by stepping finitely many times from a type to the range type of one 
of its fields. This formalization diverges from \cite[p. 106]{Poetzsch-Heffter97specification} 
in that it does not include the number of steps that are allowed to reach the second type.
Reachability of types is a static approximation of reachability in
the store. If I cannot reach the type of a location from the type of a
reference, I cannot reach the location from the reference. See lemma  
not_treach_ref_impl_not_reach› below.
›

inductive
  treach :: "Javatype  Javatype  bool"
where
  Subtype:       "U  T  treach T U"
| Attribute:     "treach T S; S  dtype f; U  rtype f   treach T U"
| ArrLength:     "treach (ArrT AT) IntgT"
| ArrElem:       "treach (ArrT AT) (at2jt AT)"
| Trans [trans]: "treach T U; treach U V  treach T V"


lemma treach_ref_l [simp,intro]: 
  assumes not_Null: "ref l  nullV"
  shows "treach (typeof (ref l)) (ltype l)"
proof (cases l)
  case (objLoc cf a)
  have "l=objLoc cf a" by fact
  moreover
  have "treach (CClassT (cls cf)) (rtype (att cf))"
    by (rule treach.Attribute [where ?f="att cf" and ?S="CClassT (cls cf)"])
       (auto intro: treach.Subtype)
  ultimately show ?thesis
    by simp
next
  case (staticLoc f)
  have "l=staticLoc f" by fact
  hence "ref l = nullV" by simp
  with not_Null show ?thesis
    by simp
next
  case (arrLenLoc T a)
  have "l=arrLenLoc T a" by fact
  then show ?thesis
    by (auto intro: treach.ArrLength)
next
  case (arrLoc T a i)
  have "l=arrLoc T a i" by fact
  then show ?thesis
    by (auto intro: treach.ArrElem)
qed

lemma treach_ref_l' [simp,intro]:
  assumes not_Null: "ref l  nullV"
  shows "treach (typeof (ref l)) (typeof (s@@l))"
proof -
  from not_Null have "treach (typeof (ref l)) (ltype l)" by (rule treach_ref_l)
  also have "typeof (s@@l)  ltype l"
    by simp
  hence "treach (ltype l) (typeof (s@@l))"
    by (rule treach.intros)
  finally show ?thesis .
qed
  

lemma reach_impl_treach: 
  assumes reach_l: "s  l reachable_from x"
  shows "treach (typeof x) (ltype l)"
using reach_l
proof (induct)
  case (Immediate l)
  have "ref l  nullV" by fact
  then show "treach (typeof (ref l)) (ltype l)"
    by (rule treach_ref_l)
next
  case (Indirect l k)
  have "treach (typeof (s@@k)) (ltype l)" by fact
  moreover
  have "ref k  nullV" by fact
  hence "treach (typeof (ref k)) (typeof (s@@k))"
    by simp
  ultimately show "treach (typeof (ref k)) (ltype l)"
    by (iprover intro: treach.Trans)
qed

lemma not_treach_ref_impl_not_reach: 
  assumes not_treach: "¬ treach (typeof x) (typeof (ref l))"
  shows "¬ s  l reachable_from x"
proof 
  assume reach_l: "s l reachable_from x"
  from this not_treach
  show False
  proof (induct)
    case (Immediate l)
    have "¬ treach (typeof (ref l)) (typeof (ref l))" by fact
    thus False by (iprover intro: treach.intros order_refl)
  next
    case (Indirect l k)
    have hyp: "¬ treach (typeof (s@@k)) (typeof (ref l))  False" by fact
    have not_Null: "ref k  nullV" by fact
    have not_k_l:"¬ treach (typeof (ref k)) (typeof (ref l))" by fact
    show False
    proof (cases "treach (typeof (s@@k)) (typeof (ref l))")
      case False thus False by (rule hyp)
    next
      case True
      from not_Null have "treach (typeof (ref k)) (typeof (s@@k))"
        by (rule treach_ref_l')
      also note True
      finally have "treach (typeof (ref k)) (typeof (ref l))" .
      with not_k_l show False ..
    qed
  qed
qed

text ‹Lemma 4.6 in \cite[p. 107]{Poetzsch-Heffter97specification}.›
lemma treach1: 
  assumes x_t: "typeof x  T" 
  assumes not_treach: "¬ treach T (typeof (ref l))"
  shows "¬ s  l reachable_from x"
proof -
  have "¬ treach (typeof x) (typeof (ref l))"
  proof 
    from x_t have "treach T (typeof x)" by (rule treach.intros)
    also assume "treach (typeof x) (typeof (ref l))"
    finally have "treach T (typeof (ref l))" .
    with not_treach show False ..
  qed
  thus ?thesis
    by (rule not_treach_ref_impl_not_reach)
qed

  
end

Theory JML

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

section ‹The Formalization of JML Operators›

theory JML imports "../Isabelle_Store/StoreProperties" begin

text ‹JML operators that are to be used in Hoare formulae can be formalized here.
›

definition
  instanceof :: "Value  Javatype  bool"  ("_ @instanceof _")
where
  "instanceof v t = (typeof v  t)"

end

Theory UnivSpec

(*  Title:       Jive Data and Store Model
    Author:      Nicole Rauch <rauch at informatik.uni-kl.de>, 2005
    Maintainer:  Nicole Rauch <rauch at informatik.uni-kl.de>
    License:     LGPL
*)

section ‹The Universal Specification›

theory UnivSpec imports "../Isabelle/JML"  begin

text ‹This theory contains the Isabelle formalization of the
program-dependent specification. This theory has to be provided by the user.
In later versions of Jive, one may be able to generate it from JML model
classes.
›

definition
aCounter :: "Value  Store  JavaInt" where
"aCounter x s =
  (if x ~= nullV & (alive x s) & typeof x = CClassT CounterImpl then
    aI ( s@@(x..CounterImpl'value) )
   else undefined)"

end