package cal;

/** Time of day on a 24 hour clock.
 * @author <put your name here>
 */
public /*@ pure @*/ class TimeOfDay implements Comparable {
    
    /**
     * Initialize this TimeOfDay object.
     */
    //@ requires 0 <= hour && hour <= 23;
    //@ requires 0 <= minutes && minutes <= 59;
    //@ ensures getHour() == hour && getMinutes() == minutes;
    public TimeOfDay(int hour, int minutes) {
        
    }
    
    /**
     * Return a TimeOfDay object representing the given morning time.
     */
    /*@ requires 0 <= hour && hour <= 11;
      @ requires 0 <= minutes && minutes <= 59;
      @ ensures \result != null && \result.getHour() == hour
      @      && \result.getMinutes() == minutes;
      @*/
   public /*@ pure @*/ static TimeOfDay am(int hour, int minutes) {

    }
    
    /**
     * Return a TimeOfDay object representing the given afternoon time.
     */
    /*@ requires 0 <= hour && hour <= 11;
      @ requires 0 <= minutes && minutes <= 59;
      @ ensures \result != null && \result.getHour() == 12+hour
      @      && \result.getMinutes() == minutes;
      @*/
    public /*@ pure @*/ static TimeOfDay pm(int hour, int minutes) {

    }
    
    /**
     * Return a TimeOfDay that is the given number of minutes in
     * the future from this time.
     * @param mins the number of minutes to add to this time.
     */
    /*@   requires 0 <= mins && mins <= 24*60;
      @   ensures \result != null;
      @   ensures \result.getHour()
      @         == (getHour() + (getMinutes()+mins)/60) % 24;
      @   ensures \result.getMinutes() == (getMinutes()+mins) % 60;
      @ for_example
      @   requires mins == 30 && getHour() == 10 && getMinutes() == 0;
      @   ensures  getHour() == 10 && getMinutes() == 30;
      @ also
      @   requires mins == 121 && getHour() == 10 && getMinutes() == 59;
      @   ensures  getHour() == 13 && getMinutes() == 0;
      @ also
      @   requires mins == 1 && getHour() == 23 && getMinutes() == 59;
      @   ensures  getHour() == 0 && getMinutes() == 0;
      @*/
    public TimeOfDay addMinutes(int mins) {

    }
    
    /**
     * Returns this time's hour.
     */
    //@ ensures 0 <= \result && \result <= 23; 
    public int getHour() {

    }

    /**
     * Returns this time's minutes.
     */
    //@ ensures 0 <= \result && \result <= 59; 
    public int getMinutes() {

    }
    
    /**
     * Is this time a morning time?
     */
    //@ ensures \result <==> getHour() < 12;
    public boolean isAM() {

    }
    
    /**
     * Is this an afternoon time?
     */
    //@ ensures \result <==> getHour() >= 12;
    public boolean isPM() {

    }
    
    /**
     * Is the other Object a TimeOfDay representing the same time as this?
     */
    /*@ also 
      @   ensures \result <==> o instanceof TimeOfDay
      @                        && ((TimeOfDay)o).getHour() == getHour()
      @                        && ((TimeOfDay)o).getMinutes() == getMinutes();
      @*/
    public boolean equals(Object o) {

    }
    
    // documentation comment inherited from java.lang.Object
    public int hashCode() {

    }
    
    /**
     * Return a String representing this time of day.
     * The string always has 4 digits, the first two are followed by a colon.
     * The time is in the 24 hour system.
     */
    /*@ also
      @   ensures \result != null
      @        && \result.length() == 5 && \result.charAt(2) == ':';
      @ ensures 0 <= Integer.parseInt(\result.substring(0,2))
      @      && Integer.parseInt(\result.substring(0,2)) <= 23;
      @ ensures 0 <= Integer.parseInt(\result.substring(3,5))
      @      && Integer.parseInt(\result.substring(3,5)) <= 59;
      @ for_example
      @   requires getHour() == 0 && getMinutes() == 5;
      @   ensures \result != null && \result.equals("00:05");
      @*/
    public String toString() {

    }
    
    /**
     * Return a String representing this time of day in AM/PM format.
     */
    /*@ ensures \result != null
      @      && \result.length() == 7 && \result.charAt(2) == ':'
      @      && (\result.charAt(5) == 'A' || \result.charAt(5) == 'P')
      @      && \result.charAt(6) == 'M';
      @ ensures 0 < Integer.parseInt(\result.substring(0,2))
      @      && Integer.parseInt(\result.substring(0,2)) <= 12;
      @ ensures 0 <= Integer.parseInt(\result.substring(3,5))
      @      && Integer.parseInt(\result.substring(3,5)) <= 59;
      @ for_example
      @   requires getHour() == 0 && getMinutes() == 5;
      @   ensures \result != null && \result.equals("12:05AM");
      @ also
      @   requires getHour() == 13 && getMinutes() == 5;
      @   ensures \result != null && \result.equals("01:05PM");
      @*/
    public String ampmString() {

    }
 
    /**
     * Return the number of minutes past midnight this time represents.
     */
    public /*@ pure @*/ int minutesPastMidnight() {

    }
    
    /**
     * Return the number of minutes between start and this time of day.
     * @param start a time earlier than or equal to this time
     */
    /*@ requires start != null && start.compareTo(this) <= 0;
      @ ensures \result == minutesPastMidnight()
      @                    - start.minutesPastMidnight();
      @*/
    public /*@ pure @*/ int minutesFrom(TimeOfDay start) {

    }
    
    /** Compare this to the given object.
     * @see java.lang.Comparable#compareTo(Object)
     * @param o the object to compare to
     * @return -1, 0, or +1 when o instanceof TimeOfDay
     * @throws ClassCastException when !(o instanceof TimeOfDay)
     */
    //@ also
    //@   ensures o instanceof TimeOfDay;
    //@   signals (ClassCastException) !(o instanceof TimeOfDay);
    public int compareTo(Object o) {

    }

    /** Return -1 if this is before t, 0 if they are equal,
     *  and +1 if this comes after t (in a given day).
     * @see #compareTo(Object)
     * @param t the time to compare to
     * @return -1, 0, or +1 depending on whether this is less than,
     * the same as, or greater than t.
     */
    //@ requires t != null;
    public int compareTo(TimeOfDay t) {

    }
}