de.uka.ilkd.key.axiom_abstraction.predicateabstraction

Class SimplePredicateAbstractionLattice

java.lang.Object

de.uka.ilkd.key.axiom_abstraction.AbstractDomainLattice

de.uka.ilkd.key.axiom_abstraction.predicateabstraction.AbstractPredicateAbstractionLattice

de.uka.ilkd.key.axiom_abstraction.predicateabstraction.SimplePredicateAbstractionLattice

All Implemented Interfaces:

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

public class SimplePredicateAbstractionLattice
extends AbstractPredicateAbstractionLattice

A lattice for all predicates accepting the given sort. This lattice consists of n + 2 elements, where n is the number of applicable predicates. The first element is a bottom element, the last a top element, and the elements in between correspond to the given predicates.

Author:

Dominic Scheurer

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.axiom_abstraction.predicateabstraction.AbstractPredicateAbstractionLattice

AbstractPredicateAbstractionLattice.AbstractPredicateLatticeIterator

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

PartialComparator.PartialComparisonResult

Field Summary

Fields

Modifier and Type	Field and Description
static java.lang.String	PREDICATE_NAME_CONBINATION_STRING
private java.util.List<AbstractionPredicate>	predicates

Constructor Summary

Constructors

Constructor and Description
SimplePredicateAbstractionLattice(java.util.List<AbstractionPredicate> applicablePredicates) Constructs a new SimplePredicateAbstractionLattice for the given list of applicable predicates.

Method Summary

Modifier and Type	Method and Description
boolean	equals(java.lang.Object obj)
protected AbstractPredicateAbstractionDomainElement	getBottomElem()
java.lang.String	getPredicateNameCombinationString()
protected AbstractPredicateAbstractionDomainElement	getTopElem()
int	hashCode()
java.util.Iterator<AbstractDomainElement>	iterator() The iterator for this lattice will first return the bottom element, then the given predicates in the order in which they have been initially supplied, and finally the top element.
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.
int	size()
java.lang.String	toString()

Methods inherited from class de.uka.ilkd.key.axiom_abstraction.predicateabstraction.AbstractPredicateAbstractionLattice

join

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

abstractFrom, compare, fromString, getSideConditionForAxiom

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Methods inherited from interface java.lang.Iterable

forEach, spliterator

Field Detail

PREDICATE_NAME_CONBINATION_STRING

public static final java.lang.String PREDICATE_NAME_CONBINATION_STRING

See Also:

Constant Field Values

predicates

private java.util.List<AbstractionPredicate> predicates

Constructor Detail

SimplePredicateAbstractionLattice

public SimplePredicateAbstractionLattice(java.util.List<AbstractionPredicate> applicablePredicates)

Constructs a new SimplePredicateAbstractionLattice for the given list of applicable predicates. The caller is responsible for making sure that none of the predicates is valid.

Parameters:

applicablePredicates - The predicates to generate the lattice from.

Method Detail

join

public AbstractDomainElement join(AbstractDomainElement a,
                                  AbstractDomainElement b)

Description copied from class: AbstractDomainLattice

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

Specified by:

join in class AbstractDomainLattice

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.

iterator

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

The iterator for this lattice will first return the bottom element, then the given predicates in the order in which they have been initially supplied, and finally the top element.

Specified by:

iterator in interface java.lang.Iterable<AbstractDomainElement>

Specified by:

iterator in class AbstractDomainLattice

size

public int size()

Returns:

The number of elements in this lattice.

equals

public boolean equals(java.lang.Object obj)

Overrides:

equals in class java.lang.Object

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

getTopElem

protected AbstractPredicateAbstractionDomainElement getTopElem()

Specified by:

getTopElem in class AbstractPredicateAbstractionLattice

Returns:

The top element of the lattice.

getBottomElem

protected AbstractPredicateAbstractionDomainElement getBottomElem()

Specified by:

getBottomElem in class AbstractPredicateAbstractionLattice

Returns:

The bottom element of the lattice.

getPredicateNameCombinationString

public java.lang.String getPredicateNameCombinationString()

Specified by:

getPredicateNameCombinationString in class AbstractPredicateAbstractionLattice

Returns:

The String which is used for combining the names of predicates for lattice types where multiple predicates determine an abstract element.