Программирование по контракту — различия между версиями
Sergej (обсуждение | вклад) (→Решение 1) |
Sergej (обсуждение | вклад) (→Решение 2) |
||
Строка 66: | Строка 66: | ||
return HOURS; | return HOURS; | ||
} | } | ||
− | |||
@Requires ({“newHOURS>= 0”,“newHOURS<= 23” }) | @Requires ({“newHOURS>= 0”,“newHOURS<= 23” }) | ||
@Ensures (“HOURS == newHOURS”) | @Ensures (“HOURS == newHOURS”) | ||
} | } |
Версия 16:07, 15 июня 2013
Программирование по контракту обеспечивает проверку предусловий и постусловий при выполнении методов классов, пользовательских функций. Также немаловажную роль в правильности написания функций играют инварианты.
Предусловие
Определение: |
Предусловие - должно быть выполнено до исполнения действия. |
Постусловие
Определение: |
Постусловие - должно быть выполнено после исполнения действия. |
Инвариант
Определение: |
Инвариант - определяет глобальные свойства некоторого класса, которые должны соблюдаться после его создания на протяжении всего времени жизни. |
Пример
Необходимо гарантировать, что данный класс будет возвращать корректные данные, либо, вообще не будет работать (Исходя из принципа «Мертвые программы не лгут»).
class Time { intHOURS; intMINUTES; intSECONDS; getHours(); { return HOURS; } getMinutes(); { return MINUTES; } getSeconds() { return SECONDS; } setHours(newHOURS); { HOURS = newHOURS; } setMinutes(newMINUTES); { MINUTES = newMINUTES; } setSeconds(newSECONDS) { 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”) }