de.rwth.domains.templates
Class LiftedCompleteLattice

java.lang.Object
  |
  +--de.rwth.domains.templates.LiftedPOSet
        |
        +--de.rwth.domains.templates.LiftedCompleteLattice

All Implemented Interfaces:

CompleteLattice, CompletePOSet, Lattice, LowerSemiLattice, POSet, PreLattice, PreLowerSemiLattice, PreUpperSemiLattice, Set, UpperSemiLattice

Direct Known Subclasses:

CFPStackLattice

public class LiftedCompleteLattice

extends LiftedPOSet

implements CompleteLattice

Class for the creation of lifted complete lattices by adding an unique additional top element to a pre lattice.

There is no check if the resulting structure fulfills the specified constraints!

Version:

$Id: LiftedCompleteLattice.java,v 1.3 2002/09/17 06:53:53 mohnen Exp $

Author:

Markus Mohnen

Inner classes inherited from class de.rwth.domains.Set

Set.Default

Field Summary

protected java.lang.Object

top The unique new top element of this lifted lattice.

Fields inherited from class de.rwth.domains.templates.LiftedPOSet

bottom, poset

Constructor Summary

LiftedCompleteLattice(POSet poset, java.lang.Object bottom, java.lang.Object top)
Lifts an existing partially ordered set to a lattice by adding newly created unique top element name "top" and newly created unique bottom element name "bottom".

LiftedCompleteLattice(PreLattice prelattice)
Lifts an existing pre lattice to a lattice by adding newly created unique top element name "top".

LiftedCompleteLattice(PreLattice prelattice, java.lang.Object top)
Lifts an existing pre lattice to a lattice by adding a top element.

LiftedCompleteLattice(PreLattice prelattice, java.lang.String toplabel)
Lifts an existing pre lattice to a lattice by adding newly created unique top element name toplabel.

Method Summary

java.lang.Object	bottom() Gets the least element of this CompleteLattice.
boolean	equals(java.lang.Object e1, java.lang.Object e2) Returns true either if both e1 and e2 are the unique top element of this set of they are equal in the underlying set.
boolean	isElement(java.lang.Object e) The method isElement returns true if e is the unique least element of this set or if e is element of the underlying set.
java.util.Iterator	iterator() The method iterator returns an Iterator of the elements of this set, staring with the unique least element.
java.util.Iterator	iteratorSkel() The method iterator returns an Iterator of the elements of this set, staring with the unique least element.
java.lang.Object	join(java.lang.Object e1, java.lang.Object e2) Computes the least upper bound of two elements in the following way: If le(e1,e2) holds then this is e2 and vice versa.
boolean	le(java.lang.Object e1, java.lang.Object e2) Returns true either if e1 is the unique top element of this set or if e1 is less or equal than e2 in the underlying set.
boolean	lt(java.lang.Object e1, java.lang.Object e2) Returns true either if e1 is the unique top element of this set and e2 is not or if e1 is less than e2 in the underlying set.
java.lang.Object	meet(java.lang.Object e1, java.lang.Object e2) Computes the greatest lower bound of two elements in the following way: If le(e1,e2) holds then this is e1 and vice versa.
long	size() The method size returns the size of the set.
long	sizeSkel() The method size returns the size of the set.
java.lang.Object	top() Gets the greatest element of this CompleteLattice.

Methods inherited from class de.rwth.domains.templates.LiftedPOSet

main

Methods inherited from class java.lang.Object

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

Field Detail

top

protected java.lang.Object top

The unique new top element of this lifted lattice.

Constructor Detail

LiftedCompleteLattice

public LiftedCompleteLattice(PreLattice prelattice,
                             java.lang.Object top)

Lifts an existing pre lattice to a lattice by adding a top element.

Parameters:

prelattice - a PreLattice value

top - an Object value

LiftedCompleteLattice

public LiftedCompleteLattice(PreLattice prelattice,
                             java.lang.String toplabel)

Lifts an existing pre lattice to a lattice by adding newly created unique top element name toplabel.

Parameters:

prelattice - a PreLattice value

toplabel - a String value

LiftedCompleteLattice

public LiftedCompleteLattice(PreLattice prelattice)

Lifts an existing pre lattice to a lattice by adding newly created unique top element name "top".

Parameters:

prelattice - a PreLattice value

LiftedCompleteLattice

public LiftedCompleteLattice(POSet poset,
                             java.lang.Object bottom,
                             java.lang.Object top)

Lifts an existing partially ordered set to a lattice by adding newly created unique top element name "top" and newly created unique bottom element name "bottom".

Parameters:

poset - a POSet value

bottom - an Object value

top - an Object value

Method Detail

equals

public boolean equals(java.lang.Object e1,
                      java.lang.Object e2)

Returns true either if both e1 and e2 are the unique top element of this set of they are equal in the underlying set.

Specified by:

equals in interface Set

Overrides:

equals in class LiftedPOSet

Parameters:

e1 - a value of type Object

e2 - a value of type Object

Returns:

true if e1 and e2 are equal in this set.

lt

public boolean lt(java.lang.Object e1,
                  java.lang.Object e2)

Returns true either if e1 is the unique top element of this set and e2 is not or if e1 is less than e2 in the underlying set.

Specified by:

lt in interface POSet

Overrides:

lt in class LiftedPOSet

Parameters:

e1 - a value of type Object

e2 - a value of type Object

Returns:

true if e1 is less than e2 in this set.

le

public boolean le(java.lang.Object e1,
                  java.lang.Object e2)

Returns true either if e1 is the unique top element of this set or if e1 is less or equal than e2 in the underlying set.

Specified by:

le in interface POSet

Overrides:

le in class LiftedPOSet

Parameters:

e1 - a value of type Object

e2 - a value of type Object

Returns:

true if e1 is less than or equal than e2 in this set.

iterator

public java.util.Iterator iterator()

The method iterator returns an Iterator of the elements of this set, staring with the unique least element.

Specified by:

iterator in interface Set

Overrides:

iterator in class LiftedPOSet

Returns:

an Iterator of all elements of this set.

sizeSkel

public long sizeSkel()

The method size returns the size of the set.

Specified by:

sizeSkel in interface Set

Overrides:

sizeSkel in class LiftedPOSet

Returns:

-1 if the underlying set has an infinite number of elements and one more than the size reported by the underlying set otherwise.

iteratorSkel

public java.util.Iterator iteratorSkel()

The method iterator returns an Iterator of the elements of this set, staring with the unique least element.

Specified by:

iteratorSkel in interface Set

Overrides:

iteratorSkel in class LiftedPOSet

Returns:

an Iterator of all elements of this set.

size

public long size()

The method size returns the size of the set.

Specified by:

size in interface Set

Overrides:

size in class LiftedPOSet

Returns:

-1 if the underlying set has an infinite number of elements and one more than the size reported by the underlying set otherwise.

isElement

public boolean isElement(java.lang.Object e)

The method isElement returns true if e is the unique least element of this set or if e is element of the underlying set.

Specified by:

isElement in interface Set

Overrides:

isElement in class LiftedPOSet

Parameters:

e - a value of type Object

Returns:

a value of type boolean

meet

public java.lang.Object meet(java.lang.Object e1,
                             java.lang.Object e2)

Computes the greatest lower bound of two elements in the following way: If le(e1,e2) holds then this is e1 and vice versa. Otherwise, its bottom().

Specified by:

meet in interface Lattice

Parameters:

e1 - a value of type Object

e2 - a value of type Object

Returns:

the greatest lower bound of e1 and e2

See Also:

Domain.checkProperties(PreLattice l)

join

public java.lang.Object join(java.lang.Object e1,
                             java.lang.Object e2)

Computes the least upper bound of two elements in the following way: If le(e1,e2) holds then this is e2 and vice versa. Otherwise, its top().

Specified by:

join in interface Lattice

Parameters:

e1 - a value of type Object

e2 - a value of type Object

Returns:

the least upper bound of e1 and e2

See Also:

Domain.checkProperties(PreLattice l)

top

public java.lang.Object top()

Description copied from interface: CompleteLattice

Gets the greatest element of this CompleteLattice.

Implementations should guarantee that bottom is indeed least element of this set, this is to say that isElement recognises the value returned by bottom and lt(bottom(),e)==true for all elements e.

Specified by:

top in interface CompleteLattice

Following copied from interface: de.rwth.domains.CompleteLattice

Returns:

the greatest element in this set

See Also:

Domain.checkProperties(CompleteLattice cl)

bottom

public java.lang.Object bottom()

Description copied from interface: CompleteLattice

Gets the least element of this CompleteLattice.

Implementations should guarantee that bottom is indeed least element of this set, this is to say that isElement recognises the value returned by bottom and lt(bottom(),e)==true for all elements e.

Specified by:

bottom in interface CompleteLattice

Following copied from interface: de.rwth.domains.CompleteLattice

Returns:

the least element in this set

See Also:

Domain.checkProperties(CompleteLattice cl)