org.jutil.java.collections
Class Exists

java.lang.Object
  |
  +--org.jutil.java.collections.BooleanAccumulator
        |
        +--org.jutil.java.collections.Exists

All Implemented Interfaces:

CollectionOperator

public abstract class Exists

extends BooleanAccumulator

A boolean exists operator.

A convenience accumulator of collections that checks whether some element of a collection satisfies the criterion defined in the abstract method public boolean criterion(Object element).

As with Accumulator, this class can best be used as an anonymous inner class.

boolean bool =
  new Exists() {

       /oo
         o also public behavior
         o
         o post (* additional precondition for criterion method *)
         o
         o public model boolean isValidElement(Object element);
         o/

       /oo
         o also public behavior
         o
         o post \result == ((MyType)element.someProperty() ...)
         o/
        public boolean criterion(Object element) {
          // criterion code
        }
      }.in(collection);

Version:

$Revision: 1.13 $

Author:

Marko van Dooren

Field Summary

static java.lang.String

CVS_REVISION

Constructor Summary

Exists()

Method Summary

boolean	accumulate(java.lang.Object element, boolean acc) also public behavior post \result == acc || criterion(element);
abstract boolean	criterion(java.lang.Object element) also public behavior post ! getCollection().contains(element) => \result == false; public model boolean isValidElement(Object element); public behavior // criterion should be consistent with equals post (\forall object o1;; (\forall object o2;o2.equals(o1);criterion(o1) == criterion(o2))); Check whether the given object satisfies the criterion for this Exists accumulator
boolean	in(java.util.Collection collection) also public behavior post \result == (\exists Object o;collection.contains(o);criterion(o));
boolean	initialAccumulator() also public behavior // Returns false post \result == false;

Methods inherited from class java.lang.Object

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

Field Detail

CVS_REVISION

public static final java.lang.String CVS_REVISION

Constructor Detail

Exists

public Exists()

Method Detail

criterion

public abstract boolean criterion(java.lang.Object element)

also public behavior

post ! getCollection().contains(element) => \result == false;

public model boolean isValidElement(Object element);

public behavior

// criterion should be consistent with equals
post (\forall object o1;;
(\forall object o2;o2.equals(o1);criterion(o1) == criterion(o2)));

Check whether the given object satisfies the criterion for this Exists accumulator

initialAccumulator

public boolean initialAccumulator()

also public behavior

// Returns false
post \result == false;

Overrides:

initialAccumulator in class BooleanAccumulator

accumulate

public boolean accumulate(java.lang.Object element,
                          boolean acc)

also public behavior

post \result == acc || criterion(element);

Overrides:

accumulate in class BooleanAccumulator

Following copied from class: org.jutil.java.collections.BooleanAccumulator

Parameters:

element - The object the method will process and change the accumulator with.

acc - The accumulator for the accumulation. For the first element to be processed, the result of initialAccumulator is used. For the other elements, the result of this method applied on the previous element is used.

in

public boolean in(java.util.Collection collection)

also public behavior

post \result == (\exists Object o;collection.contains(o);criterion(o));

Overrides:

in in class BooleanAccumulator

Following copied from class: org.jutil.java.collections.BooleanAccumulator

Parameters:

collection - The collection for which the ForAll operator has to be computed.