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

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

Предусловие

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

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

Постусловие

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

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

Инвариант

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

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

Пример

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

 class Time {
   int HOURS;
   int MINUTES;
   int SECONDS;
   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”)
 }

@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[/math] [math] push[/math] [math] (Object[/math] [math] 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[/math] [math] pop() [/math]

[math] peek:[/math]

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

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

[math]Object[/math] [math] 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]