de.uka.ilkd.key.logic.sort

Class NullSort

java.lang.Object

de.uka.ilkd.key.logic.sort.NullSort

All Implemented Interfaces:

Named, Sort

public final class NullSort
extends java.lang.Object
implements Sort

There is one instance of this class per proof, representing the sort "Null". This sort is a subsort of all object sorts. Unfortunately, NullSort sometimes has to be treated as a special case, because it cannot support the method extendsSorts() (without a Services parameter) -- for this, the object would have to "know" all the object sorts, but these sorts are created only after the NullSort object itself has to be created; and immutability prevents us from filling in this information later.

Field Summary

Fields

Modifier and Type	Field and Description
private java.lang.ref.WeakReference<ImmutableSet<Sort>>	extCache
private java.lang.ref.WeakReference<Services>	lastServices
static Name	NAME
private Sort	objectSort

Fields inherited from interface de.uka.ilkd.key.logic.sort.Sort

ANY, CAST_NAME, EXACT_INSTANCE_NAME, FORMULA, INSTANCE_NAME, TERMLABEL, UPDATE

Constructor Summary

Constructors

Constructor and Description
NullSort(Sort objectSort)

Method Summary

Modifier and Type	Method and Description
java.lang.String	declarationString()
ImmutableSet<Sort>	extendsSorts() Returns the direct supersorts of this sort.
ImmutableSet<Sort>	extendsSorts(Services services) Returns the direct supersorts of this sort.
boolean	extendsTrans(Sort sort) Tells whether the given sort is a reflexive, transitive subsort of this sort.
SortDependingFunction	getCastSymbol(TermServices services) returns the cast symbol of this Sort
SortDependingFunction	getExactInstanceofSymbol(TermServices services) returns the exactinstanceof symbol of this Sort
SortDependingFunction	getInstanceofSymbol(TermServices services) returns the instanceof symbol of this Sort
boolean	isAbstract() Tells whether this sort has no exact elements.
Name	name() returns the name of this element
java.lang.String	toString()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

NAME

public static final Name NAME

objectSort

private final Sort objectSort

lastServices

private java.lang.ref.WeakReference<Services> lastServices

extCache

private java.lang.ref.WeakReference<ImmutableSet<Sort>> extCache

Constructor Detail

NullSort

public NullSort(Sort objectSort)

Method Detail

name

public Name name()

Description copied from interface: Named

returns the name of this element

Specified by:

name in interface Named

Returns:

the name of the element

extendsSorts

public ImmutableSet<Sort> extendsSorts()

Description copied from interface: Sort

Returns the direct supersorts of this sort. Not supported by NullSort.

Specified by:

extendsSorts in interface Sort

extendsSorts

public ImmutableSet<Sort> extendsSorts(Services services)

Description copied from interface: Sort

Returns the direct supersorts of this sort.

Specified by:

extendsSorts in interface Sort

extendsTrans

public boolean extendsTrans(Sort sort)

Description copied from interface: Sort

Tells whether the given sort is a reflexive, transitive subsort of this sort.

Specified by:

extendsTrans in interface Sort

isAbstract

public boolean isAbstract()

Description copied from interface: Sort

Tells whether this sort has no exact elements.

Specified by:

isAbstract in interface Sort

getCastSymbol

public final SortDependingFunction getCastSymbol(TermServices services)

Description copied from interface: Sort

returns the cast symbol of this Sort

Specified by:

getCastSymbol in interface Sort

getInstanceofSymbol

public final SortDependingFunction getInstanceofSymbol(TermServices services)

Description copied from interface: Sort

returns the instanceof symbol of this Sort

Specified by:

getInstanceofSymbol in interface Sort

getExactInstanceofSymbol

public final SortDependingFunction getExactInstanceofSymbol(TermServices services)

Description copied from interface: Sort

returns the exactinstanceof symbol of this Sort

Specified by:

getExactInstanceofSymbol in interface Sort

toString

public final java.lang.String toString()

Overrides:

toString in class java.lang.Object

declarationString

public java.lang.String declarationString()

Specified by:

declarationString in interface Sort