de.uka.ilkd.key.axiom_abstraction.boollattice

Class BooleanLattice

java.lang.Object

de.uka.ilkd.key.axiom_abstraction.AbstractDomainLattice

de.uka.ilkd.key.axiom_abstraction.boollattice.BooleanLattice

All Implemented Interfaces:

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

public class BooleanLattice
extends AbstractDomainLattice

A simple lattice for booleans.

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
static AbstractDomainElement[]	ABSTRACT_DOMAIN_ELEMS All elements of this abstract domain.
private static BooleanLattice	INSTANCE The singleton instance of the lattice.

Constructor Summary

Constructors

Modifier	Constructor and Description
private	BooleanLattice() Private constructor: Singleton.

Method Summary

Modifier and Type	Method and Description
static BooleanLattice	getInstance()
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).
AbstractDomainElement	join(AbstractDomainElement elem1, AbstractDomainElement elem2) 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 de.uka.ilkd.key.axiom_abstraction.AbstractDomainLattice

abstractFrom, compare, fromString, getSideConditionForAxiom

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

ABSTRACT_DOMAIN_ELEMS

public static final AbstractDomainElement[] ABSTRACT_DOMAIN_ELEMS

All elements of this abstract domain.

INSTANCE

private static final BooleanLattice INSTANCE

The singleton instance of the lattice.

Constructor Detail

BooleanLattice

private BooleanLattice()

Private constructor: Singleton.

Method Detail

getInstance

public static BooleanLattice getInstance()

Returns:

The singleton instance of this lattice.

join

public AbstractDomainElement join(AbstractDomainElement elem1,
                                  AbstractDomainElement elem2)

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:

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

elem2 - 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()

Description copied from class: AbstractDomainLattice

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>

Specified by:

iterator in class AbstractDomainLattice