Package de.uka.ilkd.key.ldt

This package contains the "language data types" (LDTs) of KeY.

See: Description

Class Summary

Class	Description
BooleanLDT	This class inherits from LDT and implements all method that are necessary to handle the primitive type boolean.
CharListLDT
DoubleLDT	Complete this class if you want to add support for the Java double type.
FloatLDT	Complete this class if you want to add support for the Java float type.
FreeLDT	Generic data type, which has no predefined theory.
HeapLDT	LDT responsible for the "Heap" sort, and the associated "Field" sort.
IntegerLDT	This class inherits from LDT and implements all method that are necessary to handle integers, shorts and bytes.
LDT	An "LDT" or "language data type" class corresponds to a standard rule file shipped with KeY.
LocSetLDT
MapLDT	LDT for maps.
PermissionLDT
RealLDT	Complete this class if you want to add support for the JML \real type.
SeqLDT

Package de.uka.ilkd.key.ldt Description

This package contains the "language data types" (LDTs) of KeY. LDTs correspond to standard rule files shipped with KeY, and provide a programming interface to access the entities declared in these rule files.