Problem 5

Compute the angles of the clock hands for a given time of the day.

The 00:00:00 corresponds to the angle zero, increasing to the right. (This was not part of the original problem statement, but we introduce it here for simplicity of the solution.)

(We change slightly the statement so that it focuses on what we thought the “core” part of the problem. The original problem additionally concerns the drawing of the clock hands in the GUI which we intentionally leave out as Java-specific and not relevant in terms of contracts.)

Functions:

compute_angles(hour, minute, second)

Compute the angles of the clock hands for a given time of the day.
compute_angles(hour: int, minute: int, second: int) → Tuple[float, float, float][source]

Compute the angles of the clock hands for a given time of the day.

Requires

  • 0 <= second < 60

  • 0 <= minute < 60

  • 0 <= hour <= 23

Ensures
  • not (minute == 0 and second == 0)
or (result[1] == 0.0 and result[2] == 0.0)

  • second / 60 * 360 <= result[2] < (second + 1) / 60 * 360

    (Second hand between two second ticks)

  • minute / 60 * 360 <= result[1] < (minute + 1) / 60 * 360

    (Minute hand between two minute ticks)

  • (
        clock_hour := hour if hour < 12 else hour - 12,
        clock_hour / 12 * 360 <= result[0] < (clock_hour + 1) / 12 * 360
)[1]

    (Hour hand between two hour ticks)

  • not (hour == 0 and minute == 0 and second > 0)
or result[0] > 0 and result[1] > 0 and result[2] > 0

    (All hands of a clock move when the hand for seconds moves)

  • not (hour == 0 and minute == 0 and second == 0)
or result[0] == 0 and result[1] == 0 and result[2] == 0

    (Angles start from 00:00:00)

  • all(0 <= angle < 360 for angle in result)