org.jutil.java.collections
Class ForAll

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

All Implemented Interfaces:

CollectionOperator

public abstract class ForAll

extends BooleanAccumulator

A boolean for-all operator.

A convenience accumulator of collections that checks whether all elements of a collection satisfy 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 ForAll() {
       /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);

Field Summary
static java.lang.String	CVS_REVISION

 

Constructor Summary

ForAll()

 

Method Summary
boolean	accumulate(java.lang.Object element, boolean acc)
abstract  boolean	criterion(java.lang.Object element)           Check whether the given object satisfies the criterion for this ForAll accumulator.
boolean	in(java.util.Collection collection)           Perform the accumulation defined in public boolean accumulate(Object element, boolean acc) for each element of .
boolean	initialAccumulator()

 

Methods inherited from class java.lang.Object

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

 

Methods inherited from interface org.jutil.java.collections.CollectionOperator

isValidElement

 

Field Detail

CVS_REVISION

public static final java.lang.String CVS_REVISION

ForAll

public ForAll()

criterion

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

Check whether the given object satisfies the criterion for this ForAll accumulator.

Specifications:

public behavior
requires isValidElement(element);
ensures ( \forall Object o1; ; ( \forall Object o2; o2.equals(o1); criterion(o1) == criterion(o2)));

initialAccumulator

public final boolean initialAccumulator()

Specifications:

     also

public behavior
ensures \result == true;

Specifications inherited from overridden method in class BooleanAccumulator:
      --- None ---

accumulate

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

Specifications:

     also

public behavior
ensures \result == (acc&&criterion(element));

Specifications inherited from overridden method in class BooleanAccumulator:

public behavior
requires isValidElement(element);

in

public boolean in(java.util.Collection collection)

Description copied from class: BooleanAccumulator

Perform the accumulation defined in public boolean accumulate(Object element, boolean acc) for each element of . For the first element, the object returned by public boolean initialAccumulator() is used as accumulator. For the other elements, the result of the application of public boolean accumulate(Object element, boolean acc) on the previous element is used as accumulator.

The contents of is not changed.

The result of this method is the object returned by the application of public boolean accumulate(Object element, boolean acc) on the last element of the collection to be processed.

The precondition is variable. Subclasses could strengthen the postcondition of isValidElement. To the user, this means that this method cannot be called safely in a polymorphic context, since she has no idea what the actual precondition will become in subclasses. This can be resolved by making the model method isValidElement final in the polymorph supertype she needs to use.

Specifications:

     also

public behavior
ensures \result == ( \forall Object o; collection.contains(o); criterion(o));

Specifications inherited from overridden method in class BooleanAccumulator:

public behavior
requires ( \forall Object o; collection.contains(o); isValidElement(o));
ensures (* the result of the accumulation is returned *);
ensures collection == null ==> \result == initialAccumulator();
signals (ConcurrentModificationException) (* The collection was modified while accumulating *);