Просмотр исходного текста страницы Программирование по контракту

Программирование по контракту обеспечивает проверку предусловий и постусловий при выполнении методов классов, пользовательских функций. Также немаловажную роль в правильности написания функций играют инварианты.  
== Предусловие ==
{{Определение
|definition=
Предусловие - должно быть выполнено до исполнения действия.
}}
== Постусловие ==
{{Определение
|definition=
Постусловие - должно быть выполнено после исполнения действия.
}}
== Инвариант ==
{{Определение
| definition=
Инвариант - определяет глобальные свойства некоторого класса, которые должны соблюдаться после его создания на протяжении всего времени жизни.
}}
== Пример ==
Необходимо гарантировать, что функции данного класса будут возвращать корректные данные, либо, вообще не будут работать.
  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, осуществляется проверка пред и пост условий для наших методов. В чем разница? Разница в том, что во втором случае это более наглядно и удобно.

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

<tex> size - </tex> число элементов

<tex> elements - </tex> массив элементов

Методы:

<tex>push - </tex> добавить элемент

<tex> pop - </tex> удалить элемент

<tex> peek - </tex> получить элемент на вершине

<tex> size - </tex> число элементов

<tex> isEmpty - </tex> проверка на пустоту

 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];
   }
 }

Инвариант:

Размер не отрицателен, <tex>size >=0</tex>

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

Контракты:

 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()