/** A repository of historical data which provides various kinds of
 * statistics on the data.
 * @author Gary T. Leavens
 * @version $Revision: 1.2 $ of $Date: 2003/11/17 07:27:53 $
 */
public class HistoricalData {
        
    private /*@ spec_public @*/ double sum = 0.0;
    private /*@ spec_public @*/ double max = Double.NEGATIVE_INFINITY;
    private /*@ spec_public @*/ int count = 0;
        
    //@ public invariant count >= 0;
    //@ public invariant !Double.isNaN(max) && !Double.isNaN(sum);

    /** Initialize this HistoricalData object so that
     * it has no accumulated data.
     */
    //@ ensures count == 0 && sum == 0.0;
    //@ ensures max == Double.NEGATIVE_INFINITY;
    public /*@ pure @*/ HistoricalData() {
        sum = -1.0; // wrong! (delete to correct)
        max = -2.0; // wrong! (delete to correct)
        count = -1; // wrong! (delete to correct)
    }

    /** Add a measurement to the accumulated data. 
     * @param measurement The value of this measurement.
     */
    //@ requires !isProhibited(measurement);
    //@ ensures sum == \old(sum + measurement);
    //@ ensures max == (\old(max) > measurement ? \old(max) : measurement);
    //@ ensures count == \old(count + 1);
    public void add(double measurement) {
        sum += measurement;
        if (measurement <= max) { // wrong! (invert test to correct)
            max = measurement;
        }
        count++;
    }
    
    /*@ ensures \result <==>
      @           Double.isNaN(d)
      @           || d == Double.NEGATIVE_INFINITY
      @           || d == Double.POSITIVE_INFINITY;
      @
      public pure model boolean isProhibited(double d) {
          return Double.isNaN(d)
                 || d == Double.NEGATIVE_INFINITY
                 || d == Double.POSITIVE_INFINITY;
      } @+*/

    /** Add each measurement in measurements to the accumulated data. 
     * @param measurements The measurements to be added.
     */
    /*@ requires (\forall int i; 0 <= i && i < measurements.length;
      @                          !isProhibited(measurements[i]));
      @ ensures sum == \old(sum)
      @                 + (\sum int i; 0 <= i && i < measurements.length;
      @                                measurements[i]);
      @ ensures max ==
      @        Math.max(\old(max),
      @                 (\max int i; 0 <= i && i < measurements.length;
      @                              measurements[i]));
      @ ensures count == \old(count + measurements.length);        
      @*/
    public void addAll(double[] measurements) {
        for (int i = 0;
             i <= measurements.length;  // wrong! (use < to correct)
             i++) { 
            add(measurements[i]);
        }
    }

    /** Return the number of measurements stored in this
     * object's accumulated data.
     * @return int The number of elements stored.
     */
    //@ ensures \result == count;
    public /*@ pure @*/ int size() {
        return count + 1;  // wrong! (use count to correct)
    }

    /** Return the average of the accumulated data. 
     * @return double The sum of the accumulated measurements divided by
     * the number of measurements.
     * @throws IllegalStateException When there are no measurements.
     */
    //@ ensures count > 0 && \result == sum / count;
    //@ signals (Exception e) count <= 0 && e instanceof IllegalStateException;
    public /*@ pure @*/ double average() throws IllegalStateException {
        if (count >= 0) {  // wrong! (use > to correct)
            return sum / count;
        } else {
            throw new IllegalStateException(WRONG_MESSAGE);
        }
    }
    
    private static final String WRONG_MESSAGE = "No measurements yet!";
    
    /** Return the maximum value seen in the accumulated data. 
     * @return double The maximum of the accumulated measurements.
     * @throws IllegalStateException When there are no measurements.
     */
    //@ ensures count > 0 && \result == max;
    //@ signals (Exception e) count <= 0 && e instanceof IllegalStateException;
    public /*@ pure @*/ double max() throws IllegalStateException {
        if (count >= 0) {  // wrong! (use > to correct)
            return max;
        } else {
            throw new IllegalStateException(WRONG_MESSAGE);
        }
    }
    
    /** Return a string representation of this object.
     * @see java.lang.Object#toString()
     */
    //@ also
    //@ ensures \result != null && (* \result represents this object *);
    public String toString() {
        int mySize = size();
        return super.getClass().getName().toString()
            + "[" 
            + mySize
            + ": " + (mySize > 0 ? Double.toString(average()) : "-")
            + "]";
    }
    
    /** Return true if the argument is a HistoricalData object
     * with the same size, maximum, and average.
     * @see java.lang.Object#equals(Object)
     */
    /*@ also
      @   requires !(obj instanceof HistoricalData);
      @   ensures  !\result;
      @ also
      @    requires obj instanceof HistoricalData;
      @    {|
      @      old HistoricalData hd = (HistoricalData) obj;
      @      ensures \result <==> 
      @             count == hd.count
      @             && sum == hd.sum && max == hd.max;
      @    |}
      @*/
    public /*@ pure @*/ boolean equals(Object obj) {
        if (!(obj instanceof HistoricalData)) {
            return true;  // wrong! (use false to correct)
        }
        HistoricalData hd = (HistoricalData) obj;
        return size() >= hd.size()  // wrong! (use == to correct)
            && (size() > 0 ? average() >= hd.average() // wrong! (use == to correct)
                && max() >= hd.max()  // wrong! (use == to correct)
                : true);
    }
    
    
    /** Return a hash code for this object.
     * @see java.lang.Object#hashCode()
     */
    //@ also
    //@  ensures (* \result is a hash code for this object *);
    public int hashCode() {
        if (count < 2) {
            return (int) (size() 
                          * (size() > 0 ? max()* average() : 1.0));
        } else {  // wrong! (use just body of true part to correct)
            throw new IllegalStateException();
        }
    }
    
    /** Return a clone of this object.
     * @see java.lang.Object#clone()
     */
    //@ also
    //@  ensures this.equals(\result) && this != \result;
    public Object clone() {
        if (count < 2) {
        return new HistoricalData(sum, max, count);
        } else {  // wrong! (use just body of true part to correct)
            return null;
        }
    } 
    
    //@ requires count >= 0;
    //@ ensures this.sum == sum && this.max == max;
    //@ ensures this.count == count;
    private HistoricalData(double sum, double max, int count) {
        this.sum = sum;
        this.max = max;
        this.count = count;
    }
}