de.uka.ilkd.key.axiom_abstraction.signanalysis

Class Bottom

java.lang.Object

de.uka.ilkd.key.axiom_abstraction.AbstractDomainElement

de.uka.ilkd.key.axiom_abstraction.signanalysis.SignAnalysisDomainElem

de.uka.ilkd.key.axiom_abstraction.signanalysis.Bottom

All Implemented Interfaces:

Named

public class Bottom
extends SignAnalysisDomainElem

The Bottom element of the sign lattice, representing no number at all.

Author:

Dominic Scheurer

Field Summary

Fields

Modifier and Type	Field and Description
private static Bottom	INSTANCE

Constructor Summary

Constructors

Modifier	Constructor and Description
private	Bottom()

Method Summary

Modifier and Type	Method and Description
Term	getDefiningAxiom(Term varOrConst, Services services) Return the defining axiom, instantiated for a given Term (skolem constant or logical / program variable).
static Bottom	getInstance()
Name	name() returns the name of this element
java.lang.String	toParseableString(Services services) Returns a parseable String representation of this AbstractDomainElement.

Methods inherited from class de.uka.ilkd.key.axiom_abstraction.signanalysis.SignAnalysisDomainElem

isBottom, isGeq, isLeq, isNeg, isPos, isTop, isZero

Methods inherited from class de.uka.ilkd.key.axiom_abstraction.AbstractDomainElement

toString

Methods inherited from class java.lang.Object

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

Field Detail

INSTANCE

private static final Bottom INSTANCE

Constructor Detail

Bottom

private Bottom()

Method Detail

getInstance

public static Bottom getInstance()

name

public Name name()

Description copied from interface: Named

returns the name of this element

Returns:

the name of the element

getDefiningAxiom

public Term getDefiningAxiom(Term varOrConst,
                             Services services)

Description copied from class: AbstractDomainElement

Return the defining axiom, instantiated for a given Term (skolem constant or logical / program variable). The term can be seen as a representative of this abstract domain element; the returned formula must formally specify this.

If this element describes, for instance, all numbers divisible by 2, the method could return the formula "varOrConst % 2 == 0".

Specified by:

getDefiningAxiom in class AbstractDomainElement

Parameters:

varOrConst - The logical / program variable or skolem constant representing an instance of this abstract domain element.

services - A services object.

Returns:

A JavaDL formula expressing that the given variable or constant represents an instance of this abstract domain element.

toParseableString

public java.lang.String toParseableString(Services services)

Description copied from class: AbstractDomainElement

Returns a parseable String representation of this AbstractDomainElement. It should always hold that, for an AbstractDomainElement e and the corresponding AbstractDomainLattice l, that l.fromString(e.toParseableString(), services).equals(e).

Specified by:

toParseableString in class AbstractDomainElement

Parameters:

services - The services object.

Returns:

A parseable String representation of this domain element.