Theory Attributes

(*  Title:       Jive Data and Store Model
    ID:          $Id: Attributes.thy,v 1.4 2006/05/18 14:19:23 lsf37 Exp $
    Author:      Norbert Schirmer <schirmer at informatik.tu-muenchen.de>, 2003
    Maintainer:  Nicole Rauch <rauch at informatik.uni-kl.de>
    License:     LGPL
*)

header {* Attributes *}

theory Attributes imports 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. *}
constdefs dtype:: "AttId => Javatype"
"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}.
  *}
  
constdefs cDTypeId :: "AttId => CTypeId"
"cDTypeId f ≡ (case f of 
              CounterImpl'value => CounterImpl
            | UndoCounter'save => UndoCounter
            | Dummy'dummy => arbitrary
            | Counter'dummy => arbitrary )"

constdefs aDTypeId:: "AttId => ATypeId"
"aDTypeId f ≡ (case f of 
              CounterImpl'value => arbitrary
            | UndoCounter'save => arbitrary
            | Dummy'dummy => Dummy
            | Counter'dummy => arbitrary )"

constdefs iDTypeId:: "AttId => ITypeId"
"iDTypeId f ≡ (case f of 
              CounterImpl'value => arbitrary
            | UndoCounter'save => arbitrary
            | Dummy'dummy => arbitrary
            | 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.
*}
constdefs rtype:: "AttId => Javatype"
"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 @{text "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 @{text "CounterImpl"} cannot have a @{text "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 
@{text "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 @{text "CAttId"}.

  While @{text AttId} describes which fields 
are declared in which classes and interfaces,
  @{text CAttId} describes which objects of which classes may contain which 
fields at run-time. Thus,
  @{text 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 @{text "catt"} builds a @{text "CAttId"} from a class name
and a field name. In case of the illegal combinations we just return
@{text "arbitrary"}. We can also filter out static fields in 
@{text "catt"}.*}
  
constdefs catt:: "CTypeId => AttId => CAttId"
"catt C f ≡
  (case C of
     CounterImpl => (case f of 
                CounterImpl'value => CounterImpl'CounterImpl'value
              | UndoCounter'save => arbitrary
              | Dummy'dummy => arbitrary
              | Counter'dummy => CounterImpl'Counter'dummy)
   | UndoCounter => (case f of 
                     CounterImpl'value => UndoCounter'CounterImpl'value
                   | UndoCounter'save => UndoCounter'UndoCounter'save
                   | Dummy'dummy => arbitrary
                   | Counter'dummy => UndoCounter'Counter'dummy)
   | Object => arbitrary
   | Exception => arbitrary
   | ClassCastException => arbitrary
   | NullPointerException => arbitrary
)"


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. *}
  
constdefs cls:: "CAttId => CTypeId"
"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. *}
constdefs att:: "CAttId => AttId"
"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