KeY Logic Documentation

Defined symbols in the KeY System

Generated from version: heads/main on Sat Mar 01 14:33:17 UTC 2025

Overview

locSets.key

Sorts

LocSet

LocSet;defined in: locSets.key Line: 9 Offset :4

Functions

empty

\unique LocSet empty ; defined in: locSets.key Line: 14 Offset :4

allLocs

\unique LocSet allLocs ; defined in: locSets.key Line: 15 Offset :4

singleton

LocSet singleton (Object , Field ); defined in: locSets.key Line: 18 Offset :4

union

LocSet union (LocSet , LocSet ); defined in: locSets.key Line: 19 Offset :4

intersect

LocSet intersect (LocSet , LocSet ); defined in: locSets.key Line: 20 Offset :4

setMinus

LocSet setMinus (LocSet , LocSet ); defined in: locSets.key Line: 21 Offset :4

infiniteUnion

LocSet infiniteUnion {true } (LocSet ); defined in: locSets.key Line: 22 Offset :4

allFields

LocSet allFields (Object ); defined in: locSets.key Line: 23 Offset :4

allObjects

LocSet allObjects (Field ); defined in: locSets.key Line: 24 Offset :4

arrayRange

LocSet arrayRange (Object , int , int ); defined in: locSets.key Line: 25 Offset :4

freshLocs

LocSet freshLocs (Heap ); defined in: locSets.key Line: 26 Offset :4

allElementsOfArray

LocSet allElementsOfArray (Heap , Object , LocSet ); defined in: locSets.key Line: 28 Offset :4

allElementsOfArrayLocsets

LocSet allElementsOfArrayLocsets (Heap , Object , LocSet ); defined in: locSets.key Line: 29 Offset :4

Predicates

elementOf

elementOf (Object , Field , LocSet ); defined in: locSets.key Line: 33 Offset :4

subset

subset (LocSet , LocSet ); defined in: locSets.key Line: 34 Offset :4

disjoint

disjoint (LocSet , LocSet ); defined in: locSets.key Line: 35 Offset :4

createdInHeap

createdInHeap (LocSet , Heap ); defined in: locSets.key Line: 36 Offset :4