001package components.ampmclock;
002
003import components.standard.Standard;
004
005/**
006 * AMPMClock number component with primary methods.
007 *
008 * @mathsubtypes {@code
009 * HOUR_MODEL is integer
010 *  exemplar h
011 *  constraint 1 <= h <= 12
012 *
013 * MINUTE_SECOND_MODEL is integer
014 *  exemplar m
015 *  constraint 0 <= m <= 59
016 *
017 * AM_PM_CLOCK_MODEL is (
018 *   hours:   HOUR_MODEL
019 *   minutes: MINUTE_SECOND_MODEL
020 *   seconds: MINUTE_SECOND_MODEL
021 *   am:      boolean
022 *  )
023 * }
024 * @mathmodel type AMPMClock is modeled by AM_PM_CLOCK_MODEL
025 * @initially {@code
026 * ():
027 *  ensures
028 *   this.hours = 12 and
029 *   this.minutes = 0 and
030 *   this.seconds = 0 and
031 *   this.am = true
032 * (int h, int m, int s, boolean a):
033 *  requires
034 *   1 <= h <= 12 and
035 *   0 <= m <= 59 and
036 *   0 <= s <= 59
037 *  ensures
038 *   this.hours = h and
039 *   this.minutes = m and
040 *   this.seconds = s and
041 *   this.am = a
042 * }
043 */
044public interface AMPMClock extends Standard<AMPMClock> {
045
046    /**
047     * Sets {@code this.hours} to {@code newHours}.
048     *
049     * @param newHours
050     *            the new hours for {@code this}
051     * @replaces this.hours
052     * @requires {@code 1 <= newHours <= 12}
053     * @ensures this.hours = newHours
054     */
055    void setHours(int newHours);
056
057    /**
058     * Sets {@code this.minutes} to {@code newMinutes}.
059     *
060     * @param newMinutes
061     *            the new minutes for {@code this}
062     * @replaces this.minutes
063     * @requires {@code 0 <= newMinutes <= 59}
064     * @ensures this.minutes = newMinutes
065     */
066    void setMinutes(int newMinutes);
067
068    /**
069     * Sets {@code this.seconds} to {@code newSeconds}.
070     *
071     * @param newSeconds
072     *            the new seconds for {@code this}
073     * @replaces this.seconds
074     * @requires {@code 0 <= newSeconds <= 59}
075     * @ensures this.seconds = newSeconds
076     */
077    void setSeconds(int newSeconds);
078
079    /**
080     * Sets {@code this.am} to {@code am}.
081     *
082     * @param am
083     *            the new am for {@code this}
084     * @replaces this.am
085     * @ensures this.am = am
086     */
087    void setAM(boolean am);
088
089    /**
090     * Reports {@code this.hours}.
091     *
092     * @return {@code this.hours}
093     * @ensures hours = this.hours
094     */
095    int hours();
096
097    /**
098     * Reports {@code this.minutes}.
099     *
100     * @return {@code this.minutes}
101     * @ensures minutes = this.minutes
102     */
103    int minutes();
104
105    /**
106     * Reports {@code this.seconds}.
107     *
108     * @return {@code this.seconds}
109     * @ensures seconds = this.seconds
110     */
111    int seconds();
112
113    /**
114     * Reports {@code this.am}.
115     *
116     * @return {@code this.am}
117     * @ensures isAM = this.am
118     */
119    boolean isAM();
120
121}