de.uka.ilkd.key.axiom_abstraction

Class AbstractDomainElement

java.lang.Object

de.uka.ilkd.key.axiom_abstraction.AbstractDomainElement

All Implemented Interfaces:

Named

Direct Known Subclasses:

AbstractPredicateAbstractionDomainElement, BooleanDomainElem, SignAnalysisDomainElem

public abstract class AbstractDomainElement
extends java.lang.Object
implements Named

An element of an abstract domain. Elements are described by defining axioms; the main function of this class is to create such defining axioms for given terms, usually Skolem constants or program variables.

Author:

Dominic Scheurer

Constructor Summary

Constructors

Constructor and Description
AbstractDomainElement()

Method Summary

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

Methods inherited from class java.lang.Object

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

Methods inherited from interface de.uka.ilkd.key.logic.Named

name

Constructor Detail

AbstractDomainElement

public AbstractDomainElement()

Method Detail

getDefiningAxiom

public abstract Term getDefiningAxiom(Term varOrConst,
                                      Services services)

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".

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 abstract java.lang.String toParseableString(Services services)

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).

Parameters:

services - The services object.

Returns:

A parseable String representation of this domain element.

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object