Time.java

interface Time {
  // ...

  @Ensures({
    "result >= 0",
    "result <= 23"
  })
  int getHour();

  @Requires({
    "newHour >= 0",
    "newHour <= 23"
  })
  @Ensures("getHour() == newHour")
  void setHour(int newHour);

  // ...
}