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

alpha::select

alpha alpha :: select (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

alpha::defaultValue

alpha alpha :: defaultValue ; defined in: heap.key Line: 23 Offset :4

arr

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

java.lang.Object::<transient>

\unique Field java.lang.Object :: ; defined in: heap.key Line: 27 Offset :4

java.lang.Object::<transactionConditionallyUpdated>

\unique Field java.lang.Object :: ; defined in: heap.key Line: 28 Offset :4

java.lang.Object::<created>

\unique Field java.lang.Object :: ; defined in: heap.key Line: 29 Offset :4

java.lang.Object::<initialized>

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

alpha::<classPrepared>

\unique Field alpha :: ; defined in: heap.key Line: 31 Offset :4

alpha::<classInitialized>

\unique Field alpha :: ; defined in: heap.key Line: 32 Offset :4

alpha::<classInitializationInProgress>

\unique Field alpha :: ; defined in: heap.key Line: 33 Offset :4

alpha::<classErroneous>

\unique Field alpha :: ; defined in: heap.key Line: 34 Offset :4

length

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

null

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

wellFormed

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

arrayStoreValid

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

nonNull

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

assignable

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

KeY Logic Documentation

Defined symbols in the KeY System

Overview

heap.key

Sorts