Package components.ampmclock

Interface AMPMClock

All Superinterfaces:
Standard<AMPMClock>
public interface AMPMClock extends Standard<AMPMClock>
AMPMClock number component with primary methods.
Mathematical Subtypes:
HOUR_MODEL is integer
 exemplar h
 constraint 1 <= h <= 12

MINUTE_SECOND_MODEL is integer
 exemplar m
 constraint 0 <= m <= 59

AM_PM_CLOCK_MODEL is (
  hours:   HOUR_MODEL
  minutes: MINUTE_SECOND_MODEL
  seconds: MINUTE_SECOND_MODEL
  am:      boolean
 )
Mathematical Model (abstract value and abstract invariant of this):
type AMPMClock is modeled by AM_PM_CLOCK_MODEL
Constructor(s) (initial abstract value(s) of this):
():
 ensures
  this.hours = 12 and
  this.minutes = 0 and
  this.seconds = 0 and
  this.am = true
(int h, int m, int s, boolean a):
 requires
  1 <= h <= 12 and
  0 <= m <= 59 and
  0 <= s <= 59
 ensures
  this.hours = h and
  this.minutes = m and
  this.seconds = s and
  this.am = a

  • Method Summary

    Modifier and Type
    Method
    Description
    int
    hours()
    Reports this.hours.
    boolean
    isAM()
    Reports this.am.
    int
    minutes()
    Reports this.minutes.
    int
    seconds()
    Reports this.seconds.
    void
    setAM(boolean am)
    Sets this.am to am.
    void
    setHours(int newHours)
    Sets this.hours to newHours.
    void
    setMinutes(int newMinutes)
    Sets this.minutes to newMinutes.
    void
    setSeconds(int newSeconds)
    Sets this.seconds to newSeconds.

    Methods inherited from interface components.standard.Standard

    clear, newInstance, transferFrom

  • Method Details

    • setHours

      void setHours(int newHours)
      Sets this.hours to newHours.
      Parameters:
      newHours - the new hours for this
      Replaces:
      this.hours
      Requires:
      1 <= newHours <= 12
      Ensures:
      this.hours = newHours

    • setMinutes

      void setMinutes(int newMinutes)
      Sets this.minutes to newMinutes.
      Parameters:
      newMinutes - the new minutes for this
      Replaces:
      this.minutes
      Requires:
      0 <= newMinutes <= 59
      Ensures:
      this.minutes = newMinutes

    • setSeconds

      void setSeconds(int newSeconds)
      Sets this.seconds to newSeconds.
      Parameters:
      newSeconds - the new seconds for this
      Replaces:
      this.seconds
      Requires:
      0 <= newSeconds <= 59
      Ensures:
      this.seconds = newSeconds

    • setAM

      void setAM(boolean am)
      Sets this.am to am.
      Parameters:
      am - the new am for this
      Replaces:
      this.am
      Ensures:
      this.am = am

    • hours

      int hours()
      Reports this.hours.
      Returns:
      this.hours
      Ensures:
      hours = this.hours

    • minutes

      int minutes()
      Reports this.minutes.
      Returns:
      this.minutes
      Ensures:
      minutes = this.minutes

    • seconds

      int seconds()
      Reports this.seconds.
      Returns:
      this.seconds
      Ensures:
      seconds = this.seconds

    • isAM

      boolean isAM()
      Reports this.am.
      Returns:
      this.am
      Ensures:
      isAM = this.am