Field;defined in: heap.key Line: 9 Offset :4Heap;defined in: heap.key Line: 10 Offset :4\generic alphaObj \extends Object ;defined in: heap.key Line: 11 Offset :4This function modifies a heap by changing the value in one location. It takes four arguments:
1. The heap h which is to be modified
2. The object o reference of the location which is to be modified
3. The field of the location which is to be modified
4. The value v which is to be written in the designated location.
The result is a heap which coincides with h in all locations but in (o,f), where v is stored.
In the theory of arrays, store is somtimes called "write".
The field java.lang.Object::<created> cannot be updated using store; use "create".
/*! This function modifies a heap by changing the value in one location. It takes four arguments:
1. The heap h which is to be modified
2. The object o reference of the location which is to be modified
3. The field of the location which is to be modified
4. The value v which is to be written in the designated location.
The result is a heap which coincides with h in all locations but in (o,f), where v is stored.
In the theory of arrays, store is somtimes called "write".
The field java.lang.Object::<created> cannot be updated using store; use "create". */ Heap store ( Heap , Object , Field , any ) ; defined in: heap.key Line: 19 Offset :4This function modifies a heap by changing the createdness of one object.
It takes two arguments:
1. The heap h which is to be modified
2. The object reference o for the object which is to be set created.
The result is a heap which coincides with h in all locations but in (o,java.lang.Object::
/*! This function modifies a heap by changing the createdness of one object.
It takes two arguments:
1. The heap h which is to be modified
2. The object reference o for the object which is to be set created.
The result is a heap which coincides with h in all locations but in (o,java.lang.Object::),
which has been set to true. There is no means to modify a heap by setting the createdness of an object to false.
*/ Heap create ( Heap , Object ) ; defined in: heap.key Line: 31 Offset :4This function modifies a heap by changing the value in one location. It takes three arguments: 1. The heap h which is to be modified 2. The location set s whose locations are to be modified 3. The value v which is to be written in the designated locations.
The result is a heap which coincides with h in all locations but in the locations in s where v is stored.
The field java.lang.Object::<created> cannot be updated using memset; use "create".
/*! This function modifies a heap by changing the value in one location. It takes three arguments:
1. The heap h which is to be modified
2. The location set s whose locations are to be modified
3. The value v which is to be written in the designated locations.
The result is a heap which coincides with h in all locations but in the locations in s where v is stored.
The field java.lang.Object::<created> cannot be updated using memset; use "create". */ Heap memset ( Heap , LocSet , any ) ; defined in: heap.key Line: 41 Offset :4 alpha defaultValue <[ alpha ]> ; defined in: heap.key Line: 51 Offset :4 This function turns an integer into a field reference.
Integers are used to access the entries of entries within arrays stored on the heap. This
function provides the injection of the integer domain into that of the type Field. It is
ensured that this image of arr is disjoint from any defined field constant.
The array access a[i], for instance for an int-array a, becomes int::select(heap, a, arr(i)).
/*!
This function turns an integer into a field reference.
Integers are used to access the entries of entries within arrays stored on the heap. This
function provides the injection of the integer domain into that of the type Field. It is
ensured that this image of arr is disjoint from any defined field constant.
The array access a[i], for instance for an int-array a, becomes int::select(heap, a, arr(i)).
*/ \unique Field arr ( int ) ; defined in: heap.key Line: 58 Offset :4 \unique Field $classPrepared <[ alpha ]> ; defined in: heap.key Line: 72 Offset :4 \unique Field $classInitialized <[ alpha ]> ; defined in: heap.key Line: 73 Offset :4 \unique Field $classInitializationInProgress <[ alpha ]> ; defined in: heap.key Line: 74 Offset :4 \unique Field $classErroneous <[ alpha ]> ; defined in: heap.key Line: 75 Offset :4array length
The length of an array is not stored on the heap but is an inherent property of the object reference which denotes the array.
Hence, this functions takes only one argument: the object reference whose length (as an array) is to be retrieved.
This function always results in a non-negative value.
/*! array length
The length of an array is not stored on the heap but is an inherent property of the object reference which denotes the array.
Hence, this functions takes only one argument: the object reference whose length (as an array) is to be retrieved.
This function always results in a non-negative value.
*/ int length ( Object ) ; defined in: heap.key Line: 77 Offset :4A constant holding the object reference pointing to the Java null object. Quite the same as the keyword "null" in Java.
/*! A constant holding the object reference pointing to the Java null object.
Quite the same as the keyword "null" in Java. */ Null null ; defined in: heap.key Line: 85 Offset :4 /*! This predicate takes an argument of type Heap. It is true if the following conditions hold for its the argument:
1. Every location contains a reference to a created (in this heap) object or null.
2. Every location set stored on the heap contains only created objects.
3. Every location belonging to a declared Java field holds a value compatible with its type.
4. Only finitely many objects are created on the heap.
*/ wellFormed ( Heap ) ; defined in: heap.key Line: 91 Offset :4 /*!
This predicate is true if the described array update is valid in Java.
Java has the peculiarity of covariant array types. They allow an array assignment to fail at runtime (with an ArrayStoreException). This predicate deals with the issue in the logic.
(tbd)
*/ arrayStoreValid ( any , any ) ; defined in: heap.key Line: 99 Offset :4