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


public boolean equals(nullable Object o)
equals in class Object
Specifications: pure
public behavior
ensures o == this ==> \result ;
Specifications inherited from overridden method equals(Object obj) in class Object:
public normal_behavior
requires obj != null;
ensures (* \result is true when obj is "equal to" this object *);
public normal_behavior
requires this == obj;
ensures \result ;
public code normal_behavior
requires obj != null;
ensures \result <==> this == obj;
diverges false;
ensures obj == null ==> !\result ;


public int compare(Object o,
                   Object oo)
Specifications: pure
ensures o == oo ==> \result == 0;


JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.