668
правок
Изменения
→Пример
SECONDS = newSECONDS;
}
}
Предусловие: (например для getHours) Hours >= 0 && Hours < 24.
Постусловие: возвращенное значение будет являться текущим часом.
==== Решение 1 ====
Выбрасывать исключение. Имеет недостатки: неочевидность проверки, необходимость писать кучу кода вручную.
getHours(){
if (HOURS<0 ||HOURS>23)
throw GREAT_Time_Exception ;
return HOURS;
}
==== Решение 2 ====
Java поддерживает механизм аннотаций (рекомендаций компилятору, препроцессору) – метаданные, которые могут быть добавлены в исходный код программы, не влияя на него семантически, т.е. не меняя его поведение. При этом, они могут использоваться на этапе анализа кода, компиляции и выполнения.
@Contracted // говорит о том, что класс использует контракты – для отображения в IDE
class Time
{
@Ensures ({“result >= 0”,“result <= 23” })
getHours();
{
return HOURS;
}
@Requires ({“newHOURS>= 0”,“newHOURS<= 23” })
@Ensures (“HOURS == newHOURS”)
}
