de.uka.ilkd.key.axiom_abstraction

Class AbstractDomainLattice

java.lang.Object

de.uka.ilkd.key.axiom_abstraction.AbstractDomainLattice

Type Parameters:

AbstrDomElem -

All Implemented Interfaces:

PartialComparator<AbstractDomainElement>, java.lang.Iterable<AbstractDomainElement>

Direct Known Subclasses:

AbstractPredicateAbstractionLattice, BooleanLattice, SignAnalysisLattice

public abstract class AbstractDomainLattice
extends java.lang.Object
implements PartialComparator<AbstractDomainElement>, java.lang.Iterable<AbstractDomainElement>

An abstract domain is a countable lattice with a partial order relation and a join operator. It supplies methods to abstract from a concrete domain to this abstract domain, and for iterating through the domain elements, thereby respecting the partial order.

Author:

Dominic Scheurer

Nested Class Summary

Nested classes/interfaces inherited from interface de.uka.ilkd.key.axiom_abstraction.PartialComparator

PartialComparator.PartialComparisonResult

Field Summary

Fields

Modifier and Type	Field and Description
private static int	AXIOM_PROVE_TIMEOUT_MS Time in milliseconds after which a proof attempt of a defining axiom times out.

Constructor Summary

Constructors

Constructor and Description
AbstractDomainLattice()

Method Summary

Modifier and Type	Method and Description
AbstractDomainElement	abstractFrom(SymbolicExecutionState state, Term term, Services services) Abstracts from a given element of the concrete domain by returning a suitable abstract element.
PartialComparator.PartialComparisonResult	compare(AbstractDomainElement a, AbstractDomainElement b) Compares its two arguments for order.
AbstractDomainElement	fromString(java.lang.String s, Services services) Constructs an Abstract Domain Element from the given String representation.
static Term	getSideConditionForAxiom(SymbolicExecutionState state, Term term, AbstractDomainElement elem, Services services) Returns a side condition which has to hold if elem is a correct abstraction for term.
abstract java.util.Iterator<AbstractDomainElement>	iterator() Iterates through the abstract domain elements of this abstract domain starting by the smallest element; if an element b is returned by the iterator after an element a, then either compare(a,b) == LTE, or compare(a,b) == UNDEF must hold (i.e., b may not be smaller than a).
abstract AbstractDomainElement	join(AbstractDomainElement a, AbstractDomainElement b) A lattice join operation; finds an abstract element that is the least upper bound of the set consisting of the elements a and b.

Methods inherited from class java.lang.Object

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

Methods inherited from interface java.lang.Iterable

forEach, spliterator

Field Detail

AXIOM_PROVE_TIMEOUT_MS

private static final int AXIOM_PROVE_TIMEOUT_MS

Time in milliseconds after which a proof attempt of a defining axiom times out.

See Also:

Constant Field Values

Constructor Detail

AbstractDomainLattice

public AbstractDomainLattice()

Method Detail

abstractFrom

public AbstractDomainElement abstractFrom(SymbolicExecutionState state,
                                          Term term,
                                          Services services)

Abstracts from a given element of the concrete domain by returning a suitable abstract element. The returned abstract element should be as precise as possible, that is there should not be a smaller abstract element that also describes the concrete element.

Parameters:

state - The state in which the abstraction should hold.

term - Element to abstract from.

services - The services object.

Returns:

A suitable abstract domain element.

getSideConditionForAxiom

public static Term getSideConditionForAxiom(SymbolicExecutionState state,
                                            Term term,
                                            AbstractDomainElement elem,
                                            Services services)

Returns a side condition which has to hold if elem is a correct abstraction for term.

Parameters:

state - The state in which the abstraction should hold.

term - Element to abstract from.

elem - Abstract domain element to check.

services - The services object.

Returns:

Side condition to prove in order to show that elem abstracts from term.

join

public abstract AbstractDomainElement join(AbstractDomainElement a,
                                           AbstractDomainElement b)

A lattice join operation; finds an abstract element that is the least upper bound of the set consisting of the elements a and b.

Parameters:

a - First element to find the least upper bound for.

b - Second element to find the least upper bound for.

Returns:

The least upper bound of the set consisting of the elements a and b.

compare

public PartialComparator.PartialComparisonResult compare(AbstractDomainElement a,
                                                         AbstractDomainElement b)

Description copied from interface: PartialComparator

Compares its two arguments for order. If the arguments are incomparable, UNDEF is returned. Otherwise, the method returns LTE, EQ, or GTE as the first argument is less than, equal to, or greater than the second.

Specified by:

compare in interface PartialComparator<AbstractDomainElement>

Parameters:

a - the first object to be compared.

b - the second object to be compared.

Returns:

LTE, EQ, or GTE as the first argument is less than, equal to, or greater than the second; returns UNDEF if the arguments are incomparable.

iterator

public abstract java.util.Iterator<AbstractDomainElement> iterator()

Iterates through the abstract domain elements of this abstract domain starting by the smallest element; if an element b is returned by the iterator after an element a, then either compare(a,b) == LTE, or compare(a,b) == UNDEF must hold (i.e., b may not be smaller than a).

Specified by:

iterator in interface java.lang.Iterable<AbstractDomainElement>

fromString

public AbstractDomainElement fromString(java.lang.String s,
                                        Services services)

Constructs an Abstract Domain Element from the given String representation. It should always hold that, for an AbstractDomainElement e, that fromString(e.toParseableString(), services).equals(e).

Parameters:

s - String to parse.

services - The services object.

Returns:

The corresponding AbstractDomainElement.

Throws:

java.lang.RuntimeException - if s cannot be parsed.