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

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

Предусловие

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

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

Постусловие

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

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

Инвариант

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

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

Пример

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

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

Инвариант:

hours >= 0 and hours <= 23 

minutes >= 0 and minutes < 60

seconds >= 0 and seconds < 60 

Постусловия и предусловия:

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

int getMinutes()
post: возвращенное значение будет являться текущей минутой.

int getSeconds() 
post: возвращенное значение будет являться текущей секундой.

void setHours(int newHours)
pre: 0 <= newHours <= 23
post: hours == newHours

void setMinutes(int newMinutes)
pre: 0 <= newMinutes < 60
post: minutes == newMinutes 

void setSeconds(int newSeconds)
pre: 0 <= newSeconds < 60
post: seconds == newSeconds

Решение 1

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

 void setHours(int newHours){
       if (newHours < 0 || newHours > 23) 
           throw GREAT_Time_Exception;
        hours = newHours;
 }

Решение 2

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

 @Contracted // говорит о том, что класс использует контракты – для отображения в IDE
 class Time
 {   
   void setHours(int newHours);
   {
       hours = newHours;
   }
   @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] проверка на пустоту

public class ArrayStack {
  private int size = 0;
  private Object[] elements = new Object[2];
  public void push(Object element){
      assert element != null;
      ensureCapacity(size + 1);
      elements[size++] = element;
  }
  private void ensureCapacity(int capacity) {
    if (capacity <= elements.length) {
       return;
    }
    Object[] newElements = new Object[2 * capacity];
    for (int i = 0; i < size; i++) {
        newElements[i] = elements[i];
    }
    elements = newElements;
  }
  public Object pop() {
    assert size > 0;
    return elements[--size];
  } 
  public int size() {
    return size;
  }
  public boolean isEmpty() {
    return size == 0;
  }
  public Object peek() {
    assert size > 0;
    return elements[size - 1];
  }
}

Инвариант:

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

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

Контракты:

push
pre: element != NULL 
post: size = size' + 1  and   elements[size'] == element
void push (Object  element) 

pop
pre: size > 0
post: size == size' - 1 and result == elements[size]
Object pop()

peek
pre: size > 0
post: result == elements[size - 1]
Object peek()

size
post: result == size 
int size()

isEmpty
post: result == size > 0
boolean isEmpty()