Изменения

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

435 байт добавлено, 18:41, 30 сентября 2013

→‎Пример

<tex> hours >= 0 </tex> <tex> and</tex> <tex> hours <= 23 </tex>

<tex> minutes >= 0 </tex> <tex> and</tex> <tex> minutes <= 60 </tex>

<tex> seconds >= 0 </tex> <tex> and</tex> <tex> seconds <= 60 </tex>

Постусловия и предусловия: <tex>int </tex> <tex> getHours() </tex>

<tex>post:</tex> возвращенное значение будет являться текущим часом.

<tex>post:</tex> возвращенное значение будет являться текущей секундой.

<tex> void </tex> setHours(int newHours)

<tex> pre: </tex> 0 <= newHours <= 23

<tex> post: </tex> hours == newHours

<tex> void </tex> setMinutes(int newMinutes)

<tex> pre: </tex> 0 <= newMinutes < 60

<tex> post: </tex> minutes == newMinutes

<tex> void </tex> setSeconds(int newSeconds)

<tex> pre: </tex> 0 <= newSeconds < 60

<tex> post: </tex> seconds == newSeconds

Постусловие: (например для getHours()) возвращенное значение будет являться текущим часом.

Анонимный участник