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

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

Предусловие

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

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

Постусловие

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

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

Инвариант

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

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

Пример

Необходимо гарантировать, что функции данного класса будут возвращать корректные данные, либо, вообще не будут работать.

 class Time {
   int hours;
   int minutes;
   int seconds;
   int getHours();
   {
       return hours;
   }    
   int getMinutes();
   {
       return minutes;
   }
   int getSeconds()
   {
       return seconds;
   }
   void setHours(int newHOURS);
   {
       hours = newHOURS;
   }
   void setMinutes(int newMINUTES);
   {
       minutes = newMINUTES;
   }
   void setSeconds(int newSECONDS)
   {
       seconds = newSECONDS;
   }
 }

Предусловие: (например для [math] getHours()[/math])[math] hours \gt = 0 && hours \lt = 23 [/math]. Постусловие: возвращенное значение будет являться текущим часом.

Решение 1

Выбрасывать исключение. Имеет недостатки: неочевидность проверки, необходимость писать кучу кода вручную.

 int getHours(){
       if (this.hours < 0 || this.hours > 23) 
           throw GREAT_Time_Exception;
       return hours;
 }

Решение 2

Java поддерживает механизм аннотаций (рекомендаций компилятору, препроцессору) – метаданные, которые могут быть добавлены в исходный код программы, не влияя на него семантически, т.е. не меняя его поведение. При этом, они могут использоваться на этапе анализа кода, компиляции и выполнения.

 @Contracted // говорит о том, что класс использует контракты – для отображения в IDE
 class Time
 {
   @Ensures ({“result >= 0”,“result <= 23” })
   int getHours();
   {
       return HOURS;
   }
   @Requires ({“newHOURS>= 0”,“newHOURS<= 23” })
   @Ensures (“HOURS == newHOURS”)
 }

@Requires – буквально означает, «Убедиться, что ДО выполнения подпрограммы («условие выполняется»)» Иначе – бросить исключение.

@Ensures – буквально означает, «Убедиться, что ПОСЛЕ выполнения подпрограммы ( «условие выполняется»)»

Здесь мы видим, что, как и в Решение 1, осуществляется проверка пред и пост условий для наших методов. В чем разница? Разница в том, что во втором случае это более наглядно и удобно.

Пример

Рассмотрим стек на массиве. У него есть переменные

[math] size - [/math] число элементов

[math] elements - [/math] массив элементов

Методы:

[math]push - [/math] добавить элемент

[math] pop - [/math] удалить элемент

[math] peek - [/math] получить элемент на вершине

[math] size - [/math] число элементов

[math] isEmpty - [/math] проверка на пустоту

Инвариант:

Размер не отрицателен, [math]size \gt =0[/math]

Элементы заполнены [math]elements[0..size - 1] != NULL [/math]

Контракты:

[math]push [/math]

[math]pre: element != NULL [/math]

[math]post: size = size' + 1[/math] [math] and [/math] [math] elements[size'] = element [/math] [math] void push(Object element) [/math]

[math] pop:[/math]

[math] pre: size \gt 0 [/math]

[math]post: size == size' - 1[/math] [math] and [/math] [math]result == elements[size][/math]

[math] Object pop() [/math]

[math] peek:[/math]

[math]pre: size \gt 0[/math]

[math]post: result == elements[size - 1][/math] [math] Object peek() [/math]

[math] size:[/math]

[math]post: result == size [/math]

[math]int[/math] [math] size()[/math]

[math]isEmpty:[/math]

[math]post: result == size \gt 0[/math]

[math]boolean[/math] [math]isEmpty() [/math]