Package components.ampmclock
Interface 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 TypeMethodDescriptionint
hours()
Reportsthis.hours
.boolean
isAM()
Reportsthis.am
.int
minutes()
Reportsthis.minutes
.int
seconds()
Reportsthis.seconds
.void
setAM
(boolean am) Setsthis.am
toam
.void
setHours
(int newHours) Setsthis.hours
tonewHours
.void
setMinutes
(int newMinutes) Setsthis.minutes
tonewMinutes
.void
setSeconds
(int newSeconds) Setsthis.seconds
tonewSeconds
.Methods inherited from interface components.standard.Standard
clear, newInstance, transferFrom
-
Method Details
-
setHours
Setsthis.hours
tonewHours
.- Parameters:
newHours
- the new hours forthis
- Replaces:
this.hours
- Requires:
1 <= newHours <= 12
- Ensures:
this.hours = newHours
-
setMinutes
Setsthis.minutes
tonewMinutes
.- Parameters:
newMinutes
- the new minutes forthis
- Replaces:
this.minutes
- Requires:
0 <= newMinutes <= 59
- Ensures:
this.minutes = newMinutes
-
setSeconds
Setsthis.seconds
tonewSeconds
.- Parameters:
newSeconds
- the new seconds forthis
- Replaces:
this.seconds
- Requires:
0 <= newSeconds <= 59
- Ensures:
this.seconds = newSeconds
-
setAM
Setsthis.am
toam
.- Parameters:
am
- the new am forthis
- Replaces:
this.am
- Ensures:
this.am = am
-
hours
int hours()Reportsthis.hours
.- Returns:
this.hours
- Ensures:
hours = this.hours
-
minutes
int minutes()Reportsthis.minutes
.- Returns:
this.minutes
- Ensures:
minutes = this.minutes
-
seconds
int seconds()Reportsthis.seconds
.- Returns:
this.seconds
- Ensures:
seconds = this.seconds
-
isAM
boolean isAM()Reportsthis.am
.- Returns:
this.am
- Ensures:
isAM = this.am
-