Программирование по контракту — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
(Новая страница: «Программирование по контракту обеспечивает проверку предусловий и постусловий при вып...»)
 
(Пример)
 
(не показана 91 промежуточная версия 4 участников)
Строка 1: Строка 1:
Программирование по контракту обеспечивает проверку предусловий и постусловий при выполнении методов классов, пользовательских функций.  
+
Программирование по контракту обеспечивает проверку предусловий и постусловий при выполнении методов классов, пользовательских функций. Также немаловажную роль в правильности написания функций играют инварианты. 
 
== Предусловие ==
 
== Предусловие ==
 
{{Определение
 
{{Определение
|definition
+
|definition=
 
Предусловие - должно быть выполнено до исполнения действия.
 
Предусловие - должно быть выполнено до исполнения действия.
 
}}
 
}}
 
== Постусловие ==
 
== Постусловие ==
 
{{Определение
 
{{Определение
|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()

Текущая версия на 21:29, 30 сентября 2013

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

Предусловие[править]

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

Постусловие[править]

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

Инвариант[править]

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

Пример[править]

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

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