Introduction. A completely automatic method for software verification is impossible since the problem is undecidable in general [15]. Contract validation is an important part of the software verification. Informally, a contract of a method is evaluated to true if the precondition of the method implies the postcondition of the method. If in a programming language (Java, in this paper), a standard method satisfies a given contract, it may happen that the programmer to define his own overridden method which can be error-prone at run-time. The goal of this paper is to approximate the correctness of the overridden methods with respect to its given contract. There exist many examples from Web programming, Java applets and applications [11]. In the following, we present some useful definitions, notations and examples.

In Java language, there are active classes and value classes. Active classes refer to classes that represent active entities rather than values, and for these classes, the equals() implementation provided by Object has exactly the right behavior [4]. Objects from active classes are compared according to their addresses for their identity (e.g. Thread, Random, and so on). But the situation changes when we are looking for logical equality, not object identity. This is the case for value classes, such as: Integer, Date, and so on. When two objects of a value class are compared, it is expected that equals() uses their values, rather than their references (memory addresses). For these value classes, it is necessary to override equals(). In this way, we allow instances of the class to serve as map keys or set elements with predictable and desirable behaviours.

It is important for a class to allow its objects to be sorted, especially when they will be used in specialised data structures (lists, vectors, hashtables, hashmaps, hashsets, etc). Objects that can be compared to one another are called mutually comparable. Although objects of diŽerent types can be mutually comparable, there exist Java types which cannot permit interclass comparison automatically (Byte, Character, Long, Integer, Short, Double, Float, BigInteger, BigDecimal, File, String, Date, CollationKey). However, this can be done by implementing a Java interface (Comparable) which captures the natural ordering for the objects. It contains only one method declaration, namely compareTo(Object), which compares the receiving object with the specified object and returns a negative integer, zero, or a positive integer as the receiving object is less than, equal to, or greater than the specified object. Lists (and arrays) of objects that implement this interface can be sorted automatically by Collections.sort (or Arrays.sort). Objects that implement this interface can be used as keys in a sorted map or elements in a sorted set, without the need to specify a comparator.

The equals method for class Object implements the most discriminating possible equivalence relation on objects. That is, for any reference values X and Y , this method returns true if and only if X and Y refer to the same object (X == Y has the value true). Note that it is generally necessary to override the hashCode method whenever equals() is overridden, so as to maintain the general specification for the hashCode method, which states that equal objects must have equal hash codes. Since the default implementation for equals() compares the addresses of two diŽerent objects, and not the values of the attributes, it is very likely that this will imply a violation of the consistency between equals() and hashCode() [11].

A first application where the consistency of compareTo(), equals() and hashCode() is essential, includes the classes which implement Comparable. These classes expected to be extended later as keys for HashTable, HashMap, or just used as elements in some lists where the Collections.sort() method may be applied. It is therefore necessary to implement in a consistent way all of the above functions. An important application of implementing Comparable interface is Generic Java [6]. Generic Java (GJ) is an extension of the Java programming language with support for generic types. In [7], the authors gave an example of a class which implements Comparable interface, as follows:

class Byte implements Comparable {
...
public int compareTo(Byte f) { ... }
}

They use this class to develop a generic collection class, whereby the type of the collection is known only at run-time. A similar example appears in [8], where the authors present the Java object sorting.

In [3], it is mentioned that the class String provides a good hashCode() implementation. Hash code used to be specified very explicitly in the Java Language Specification, which basically took increasingly sparse samples of the string the further it got from the start. This may imply problems with some strings, such as URLs, where the first characters are largely similar or even identical (for example, \http://"). DiŽerent virtual machines implementations may use diŽerent hashes. The current Sun distribution (for 1.4.2) seems to use a complete hash, taking into account every character, and remembers it rather than recalculating it [2], although you cannot rely upon this continuing in future releases. Thus, a possibility of creating eącient hash codes for a non-String class is to convert first its value to a String, and then using consistently the hashCode() of class String. In [3], the authors described an application which uses a HashTable object to hold attributes of a class in the form a pair (name, value). So, for a specific set of objects, it is possible to add attributes. The HashTable class uses the hashCode method to hash any object it is given as a key. No explicit hash method is needed this time, since they use String objects as keys (so the default implementation of hashCode() for String will be used) and, where the attributes have distinct names.

Another example where the keys are String is from [8]. The example refers to many different types of audio files from both applets and applications. The applet loads and holds a bunch of audio files whose locations are specified relative to a fixed base URL. Again, the keys for the hashtable are of type String corresponding to their URL. However, as we mention already above, there might be some problems regarding the efficiency of computation of the hash code for strings such as URL.