org.jutil.java.collections
Class Collections

java.lang.Object
  |
  +--org.jutil.java.collections.Collections

public abstract class Collections

extends java.lang.Object

A utility class for perform operations on collections similar to java.util.Collections.

Class Specifications

public invariant_redundantly ( \forall Collection c; c != null; ( \forall Object o1; c.contains(o1); ( \exists Object o2; containsExplicitly(c,o2); ((o1 == null)&&(o2 == null))||((o1 != null)&&(o1.equals(o2)))))); public invariant_redundantly ( \forall Collection c; c != null; ( \forall Object o2; containsExplicitly(c,o2); c.contains(o2)));

Field Summary
static java.lang.String	CVS_REVISION

 

Constructor Summary

Collections()

 

Method Summary
static boolean	containsExplicitly(java.util.Collection collection, java.lang.Object element)           Check whether or not the given collection contains the given element when using == for comparison instead of equals().
static boolean	identical(java.util.Collection first, java.util.Collection second)           Check whether the two given collections contain the same elements.
static boolean	identical(java.util.Map first, java.util.Map second)           Check whether the two given maps contain the same entries.
static int	nbExplicitOccurrences(java.lang.Object element, java.util.Collection collection)           Return the number of times has been added to .

 

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

Collections

public Collections()

containsExplicitly

public static boolean containsExplicitly(java.util.Collection collection,
                                         java.lang.Object element)

Check whether or not the given collection contains the given element when using == for comparison instead of equals().

Parameters:

collection - The collection

element - The element

Specifications:

public behavior
requires collection != null;
ensures \result == ( \exists int i; i >= 0&&i < collection.toArray().length; collection.toArray()[i] == element);

nbExplicitOccurrences

public static int nbExplicitOccurrences(java.lang.Object element,
                                        java.util.Collection collection)

Return the number of times has been added to .

Parameters:

element - The element of which the number of occurrences is requested.

collection - The collection in which the number of occurrences has to be counted.

Specifications:

public behavior
requires collection != null;
ensures \result == ( \num_of int i; i >= 0&&i < collection.toArray().length; collection.toArray()[i] == element);

identical

public static boolean identical(java.util.Collection first,
                                java.util.Collection second)

Check whether the two given collections contain the same elements. Test are done with ==

Parameters:

first - The first collection

second - The second collection

Specifications:

public behavior
ensures ((first == null)&&(second == null)) ==> \result == true;
ensures ((first == null)||(second == null))&&!((first == null)&&(second == null)) ==> \result == false;
ensures ((first != null)&&(second != null)) ==> \result == (first.size() == second.size())&&( \forall Object o; containsExplicitly(first,o); nbExplicitOccurrences(o,first) == nbExplicitOccurrences(o,second));

identical

public static boolean identical(java.util.Map first,
                                java.util.Map second)

Check whether the two given maps contain the same entries. Test are done with ==

Parameters:

first - The first map

second - The second map

Specifications:

ensures ((first == null)&&(second == null)) ==> \result == true;
ensures ((first == null)||(second == null))&&!((first == null)&&(second == null)) ==> \result == false;
ensures ((first != null)&&(second != null)) ==> \result == (first.size() == second.size())&&( \forall Object k; first.containsKey(k); second.containsKey(k)&&second.get(k) == first.get(k))&&first.size() == second.size();
ensures ( \forall Map.Entry e1; first.entrySet().contains(e1); ( \exists Map.Entry e2; second.entrySet().contains(e2); (e1.getKey() == e2.getKey())&&(first.get(e1) == second.get(e2))));