package cal;

import java.util.*;

/** Appointments for a calendar.
 * @author <put your name here>
 */
public class Appointment implements Cloneable {
   
    /**
     * Initialize this appointment to be at 8AM for 60 minutes in
     * "my office", with the person being met the empty string.
     */
    /*@ ensures getStart() != null && getStart().getHour() == 8
      @      && getStart().getMinutes() == 0 && getLength() == 60
      @      && getLocation() != null && getWho() != null
      @      && getLocation().equals("my office")
      @      && getWho().equals("");
      @*/
    public Appointment() {      

    }

    /**
     * Returns the length of this appointment in minutes.
     */
    //@ ensures \result >= 0;
    public /*@ pure @*/ int getLength() {

    }

    /**
     * Returns the starting time of the meeting.
     */
    //@ ensures \result != null;
    public /*@ pure @*/ TimeOfDay getStart() {

    }

    /**
     * Returns the ending time of the meeting.
     */
    //@ ensures \result != null;
    public /*@ pure @*/ TimeOfDay getEnd() {

    }
    
    /**
     * Returns the location of the meeting.
     */
    //@ ensures \result != null;
    public /*@ pure @*/ String getLocation() {

    }

    /**
     * Returns the person or persons being met.
     */
    //@ ensures \result != null;
    public /*@ pure @*/ String getWho() {

    }

    /**
     * Sets the length of the meeting.
     * The start time of the meeting is unchanged,
     * but the ending time of the meeting is changed
     * to take the new length into account.
     * @param minutes The length of the meeting.
     */
    //@ requires minutes > 0;
    //@ ensures getLength() == minutes;
    //@ ensures getEnd().equals(getStart().addMinutes(minutes));
    //@ ensures getStart().equals(\old(getStart()));
    public void setLength(int minutes) {

    }

    /**
     * Sets the start time of the meeting to the given time.
     * The length of the meeting stays the same,
     * but the end time may change to compensate.
     * @param start The starting time desired
     */
    //@ requires start != null;
    //@ ensures getStart().equals(start);
    //@ ensures getLength() == \old(getLength());
    //@ ensures getEnd().equals(start.addMinutes(getLength()));
    public void setStart(TimeOfDay start) {

    }

    /**
     * Sets the end time of the meeting to the given time.
     * Note that the end time must be no earlier than the start time.
     * The length of the meeting is changed to take the new ending time
     * into account.
     * @param end The ending time desired
     */
    //@ requires end != null && end.compareTo(getStart()) >= 0;
    //@ ensures getEnd().equals(end);
    //@ ensures getStart().equals(\old(getStart()));
    //@ ensures getLength() == end.minutesFrom(getStart());
    public void setEnd(TimeOfDay end) {

    }

    /**
     * Sets the location of the meeting.
     * @param location The meeting location.
     */
    //@ requires location != null;
    //@ ensures getLocation().equals(location);
    public void setLocation(String location) {

    }

    /**
     * Sets the person or persons being met.
     * @param who The person being met.
     */
    //@ requires who != null;
    //@ ensures getWho().equals(who);
    public void setWho(String who) {

    }
    
    // equals and hashCode are inherited, because this type is mutable
    
    /** Return a (shallow) clone of this object. */
    /*@ also
      @   ensures \result instanceof Appointment;
      @*/
    public Object clone() {

    }
    
    /** Return a string of the form
     *   "At 10:00PM in 229 Atanasoff meet Francis for 50 min"
     * that describes the appointment. 
     * Note that when the location or the person is the empty string,
     * then there will be two blanks next to each other in the result,
     * for example new Appointment().toString() returns
     *   "At 08:00AM in my office meet  for 60 min" 
     */
    /*@ also
      @   ensures \result != null && \result.length() >= 27;
      @*/
    public String toString() {

    }

}