org.jutil.java.collections
Interface CollectionOperator

All Known Implementing Classes:

Accumulator, BooleanAccumulator, Filter, IntegerAccumulator, Mapping, RobustVisitor, Visitor

public interface CollectionOperator

CollectionOperator is the toplevel interface for collection operators.

To be able to prove the correctness of a subclass, a model method is provided which acts like an abstract precondition for methods that operate on the elements of collections.

Collection operators are typically used as anonymous inner classes, in which case some assertions are known to be true for the collection. It would be inconvenient if those assertions would have to be repeated in the isValidElement method. If the isValidElement method has access to the collection on which the operator is used, the assertions don't have to be repeated if the object of the anonymous inner class cannot escape from the method it is defined in, and if the anonymous inner class itself does not modify the collection. In this case, the postcondition must simply say that the given parameter must be in that collection. If it could be used outside the scope of the method, the assertions which the anonymous inner class counts on, could be violated.

The method is typically used as follows for anonymous inner classes:

 /oo
   o also public behavior
   o
   o post \result == local_collection_variable.contains(element);
   o
   o public model boolean isValidElement(Object element);
   oo/

This way, the assertions for local_collection_variable are implicitly "copied" to the precondition for the methods which operate on the elements.

If the class is used in a general context, the limits on the elements have to be written explicitly:

 /oo
   o also public behavior
   o
   o post \result == (element instanceof MyType) &&
   o                 (element != null) &&
   o                   (* some other condition *);
   o
   o public model boolean isValidElement(Object element);
   oo/
 

Version:

$Revision: 1.6 $

Author:

Marko van Dooren

Field Summary

static java.lang.String

CVS_REVISION

Field Detail

CVS_REVISION

public static final java.lang.String CVS_REVISION