java.util
Interface Comparator

All Known Implementing Classes:

JCompilationUnit.JCompilationUnit$2, JCompilationUnit.JCompilationUnit$3, MjExecutableMemberDoc.Comp

public interface Comparator

Class Specifications

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Method Summary
int	compare(Object o, Object oo)
boolean	equals(nullable Object o)

 

Method Detail

equals

public boolean equals(nullable Object o)

Overrides:

equals in class Object

Specifications: pure

     also

public behavior
ensures o == this ==> \result ;

Specifications inherited from overridden method equals(Object obj) in class Object:
       pure

public normal_behavior
requires obj != null;
ensures (* \result is true when obj is "equal to" this object *);

     also

public normal_behavior
requires this == obj;
ensures \result ;

     also

public code normal_behavior
requires obj != null;
ensures \result <==> this == obj;

     also

diverges false;
ensures obj == null ==> !\result ;

compare

public int compare(Object o,
                   Object oo)

Specifications: pure

ensures o == oo ==> \result == 0;