Изменения

Перейти к: навигация, поиск

Программирование по контракту

453 байта добавлено, 18:34, 30 сентября 2013
Пример
}
Инвариант:
 
<tex> hours >= 0 </tex> <tex> and</tex> <tex> hours <= 23 </tex>
<tex> seconds >= 0 </tex> <tex> and</tex> <tex> seconds <= 60 </tex>
 
<tex>int getHours() </tex>
 
<tex>post:</tex> возвращенное значение будет являться текущим часом.
 
<tex>int getMinutes() </tex>
 
<tex>post:</tex> возвращенное значение будет являться текущей минутой.
 
<tex>int getSeconds() </tex>
 
<tex>post:</tex> возвращенное значение будет являться текущей секундой.
 
Постусловие: (например для getHours()) возвращенное значение будет являться текущим часом.
==== Решение 1 ====
Выбрасывать исключение. Имеет недостатки: неочевидность проверки, необходимость писать кучу кода вручную.
int void getHours(newHours){ if (this.hours newHours < 0 || this.hours newHours > 23)
throw GREAT_Time_Exception;
return hours;
Анонимный участник

Навигация