heap -- Documentation

Field

Field;defined in: heap.key Line: 9 Offset :4

Heap

Heap;defined in: heap.key Line: 10 Offset :4

alphaObj

\generic alphaObj \extends Object ;defined in: heap.key Line: 11 Offset :4

select

alpha select <[ alpha ]> (Heap , Object , Field ); defined in: heap.key Line: 16 Offset :4

store

Heap store (Heap , Object , Field , any ); defined in: heap.key Line: 17 Offset :4

create

Heap create (Heap , Object ); defined in: heap.key Line: 18 Offset :4

anon

Heap anon (Heap , LocSet , Heap ); defined in: heap.key Line: 19 Offset :4

memset

Heap memset (Heap , LocSet , any ); defined in: heap.key Line: 20 Offset :4

defaultValue

alpha defaultValue <[ alpha ]> ; defined in: heap.key Line: 23 Offset :4

final

alpha final <[ alpha ]> (Object , Field ); defined in: heap.key Line: 26 Offset :4

arr

\unique Field arr (int ); defined in: heap.key Line: 29 Offset :4

java.lang.Object::#$transient

\unique Field java.lang.Object :: #$transient ; defined in: heap.key Line: 30 Offset :4

java.lang.Object::#$transactionConditionallyUpdated

\unique Field java.lang.Object :: #$transactionConditionallyUpdated ; defined in: heap.key Line: 31 Offset :4

java.lang.Object::#$created

\unique Field java.lang.Object :: #$created ; defined in: heap.key Line: 32 Offset :4

java.lang.Object::#$initialized

\unique Field java.lang.Object :: #$initialized ; defined in: heap.key Line: 33 Offset :4

$classPrepared

\unique Field $classPrepared <[ alpha ]> ; defined in: heap.key Line: 34 Offset :4

$classInitialized

\unique Field $classInitialized <[ alpha ]> ; defined in: heap.key Line: 35 Offset :4

$classInitializationInProgress

\unique Field $classInitializationInProgress <[ alpha ]> ; defined in: heap.key Line: 36 Offset :4

$classErroneous

\unique Field $classErroneous <[ alpha ]> ; defined in: heap.key Line: 37 Offset :4

length

int length (Object ); defined in: heap.key Line: 40 Offset :4

null

Null null ; defined in: heap.key Line: 43 Offset :4

wellFormed

wellFormed (Heap ); defined in: heap.key Line: 47 Offset :4

arrayStoreValid

arrayStoreValid (any , any ); defined in: heap.key Line: 48 Offset :4

nonNull

nonNull (Heap , Object , int ); defined in: heap.key Line: 49 Offset :4

assignable

assignable (Heap , Heap , LocSet ); defined in: heap.key Line: 52 Offset :4

KeY Logic Documentation

Defined symbols in the KeY System

Overview

heap.key

Sorts