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

Программирование по контракту обеспечивает проверку предусловий и постусловий при выполнении методов классов, пользовательских функций. Также немаловажную роль в правильности написания функций играют инварианты.

Предусловие

Определение:

Предусловие - должно быть выполнено до исполнения действия.

Постусловие

Определение:

Постусловие - должно быть выполнено после исполнения действия.

Инвариант

Определение:

Инвариант - определяет глобальные свойства некоторого класса, которые должны соблюдаться после его создания на протяжении всего времени жизни.

Пример

Необходимо гарантировать, что данный класс будет возвращать корректные данные, либо, вообще не будет работать (Исходя из принципа «Мертвые программы не лгут»).

 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”)
 }