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:

Field Summary



static java.lang.String
CVS_REVISION



           


 









Method Summary



abstract  boolean
isValidPair(java.lang.Object key,
            java.lang.Object element)



          This model method is supplied to make proving the correctness of a subclass
 easier.


 














Field Detail




CVS_REVISION
public static final java.lang.String CVS_REVISION












Method Detail




isValidPair
public abstract boolean isValidPair(java.lang.Object key,
                                    java.lang.Object element)

This model method is supplied to make proving the correctness of a subclass
 easier. It offers a tunnel for information from the caller of
 methods that operate on the map.
 
Most often, this information concerns the type of the keys and elements,
 and them not being null.
 
The algorithm does not use this method, so we will not force subclasses
 to implement it. A strengthened specification should be given to enable
 proving the correctness of a specific operator.
 
This is actually an abstract precondition as used in Eiffel.


Specifications:

 public behavior

ensures ( \forall Object key1; ; ( \forall Object key2; (key2 != null)&&key2.equals(key1); ( \forall Object o1; ; ( \forall Object o2; (o2 != null)&&o2.equals(o1); isValidPair(key1,o1) == isValidPair(key2,o2)))));















  

  
    Overview 
  
    Package 
  
  Class 
  
    Tree 
  
    Deprecated 
  
    Index 
  
    Help 
  









 PREV CLASS 
 NEXT CLASS

  FRAMES   
 NO FRAMES



  SUMMARY:  INNER | FIELD | CONSTR | METHOD

DETAIL:  FIELD | CONSTR | METHOD