org.jutil.java.collections
Interface MapOperator

All Known Implementing Classes:

MapVisitor, RobustMapVisitor

public interface MapOperator

MapOperator is the toplevel interface for map 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 object-key pair of maps.

Map operators are typically used as anonymous inner classes, in which case some assertions are known to be true for the pairs in the map. It would be inconvenient if those assertions would have to be repeated in the isValidPair method. If the isValidPair method has access to the map 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 maps. In this case, the postcondition must simply say that the given pair must be in that map. 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:

 *
 * also public behavior
 *
 * post \result == (\exists Map.Entry entry; local_map_variable.entrySet().contains(entry);
 *                   entry.getKey().equals(key) && entry.getValue().equals(element));
 *
 * public model boolean isValidPair(Object key, Object element);
 *

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

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

 *
 * also public behavior
 *
 * post \result == (element instanceof MyType) &&
 * poar            (key instanceof MyType) &&
 * post            (element != null) &&
 * post            (key != null) &&
 * post            (* some other expression using both key and element *);
 *
 * public model boolean isValidPair(Object key, Object element);
 *
 

Version:

$Revision: 1.3 $

Author:

Marko van Dooren

Field Summary

static java.lang.String

CVS_REVISION

Field Detail

CVS_REVISION

public static final java.lang.String CVS_REVISION