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

Материал из Викиконспекты
Перейти к: навигация, поиск
(Пример)
м (rollbackEdits.php mass rollback)
 
(не показано 12 промежуточных версий 2 участников)
Строка 17: Строка 17:
 
== Пример ==
 
== Пример ==
 
Необходимо гарантировать, что функции данного класса будут возвращать корректные данные, либо, вообще не будут работать.
 
Необходимо гарантировать, что функции данного класса будут возвращать корректные данные, либо, вообще не будут работать.
   class Time {
+
   public class Time {
     int hours;
+
     private int hours;
     int minutes;
+
     private int minutes;
     int seconds;
+
     private int seconds;
     int getHours();
+
     public int getHours();
 
     {
 
     {
 
         return hours;
 
         return hours;
 
     }     
 
     }     
     int getMinutes();
+
     public int getMinutes();
 
     {
 
     {
 
         return minutes;
 
         return minutes;
 
     }
 
     }
     int getSeconds()
+
     public int getSeconds()
 
     {
 
     {
 
         return seconds;
 
         return seconds;
 
     }
 
     }
     void setHours(int newHOURS);
+
     public void setHours(int newHOURS);
 
     {
 
     {
 
         hours = newHOURS;
 
         hours = newHOURS;
 
     }
 
     }
     void setMinutes(int newMINUTES);
+
     public void setMinutes(int newMINUTES);
 
     {
 
     {
 
         minutes = newMINUTES;
 
         minutes = newMINUTES;
 
     }
 
     }
     void setSeconds(int newSECONDS)
+
     public void setSeconds(int newSECONDS)
 
     {
 
     {
 
         seconds = newSECONDS;
 
         seconds = newSECONDS;
Строка 48: Строка 48:
 
Инвариант:  
 
Инвариант:  
  
<tex> hours >= 0 </tex> <tex> and</tex> <tex> hours <= 23 </tex>
+
hours >= 0 and hours <= 23  
  
<tex> minutes >= 0 </tex> <tex> and</tex> <tex> minutes < 60 </tex>
+
minutes >= 0 and minutes < 60
  
<tex> seconds >= 0 </tex> <tex> and</tex> <tex> seconds < 60 </tex>
+
seconds >= 0 and seconds < 60  
  
 
Постусловия и предусловия:
 
Постусловия и предусловия:
  
  
<tex>int</tex> <tex> getHours() </tex>
+
int getHours()
 +
post: возвращенное значение будет являться текущим часом.
  
<tex>post:</tex>  возвращенное значение будет являться текущим часом.
 
  
 +
int getMinutes()
 +
post: возвращенное значение будет являться текущей минутой.
  
<tex>int</tex> <tex> getMinutes() </tex>
 
  
<tex>post:</tex>  возвращенное значение будет являться текущей минутой.
+
int getSeconds()
 +
post: возвращенное значение будет являться текущей секундой.
  
  
<tex>int</tex> <tex> getSeconds() </tex>
+
void setHours(int newHours)
 +
pre: 0 <= newHours <= 23
 +
post: hours == newHours
  
<tex>post:</tex>  возвращенное значение будет являться текущей секундой.
 
  
 +
void setMinutes(int newMinutes)
 +
pre: 0 <= newMinutes < 60
 +
post: minutes == newMinutes
  
<tex> void </tex> <tex>setHours(int</tex> <tex> newHours)</tex>
 
  
<tex> pre: </tex> <tex>0 <= newHours <= 23</tex>
+
void setSeconds(int newSeconds)
 
+
pre: 0 <= newSeconds < 60
<tex> post: </tex> <tex>hours == newHours</tex>
+
post: seconds == newSeconds
 
 
 
 
<tex> void </tex> <tex>setMinutes(int</tex> <tex>newMinutes)</tex>
 
 
 
<tex> pre: </tex> <tex>0 <= newMinutes < 60</tex>
 
 
 
<tex> post: </tex> <tex>minutes == newMinutes </tex>
 
 
 
 
 
<tex> void </tex> <tex>setSeconds(int</tex> <tex>newSeconds)</tex>
 
 
 
<tex> pre: </tex> <tex>0 <= newSeconds < 60</tex>
 
 
 
<tex> post: </tex> <tex>seconds == newSeconds</tex>
 
  
 
==== Решение 1 ====
 
==== Решение 1 ====
Строка 138: Строка 129:
  
 
  public class ArrayStack {
 
  public class ArrayStack {
   private int size;
+
   private int size = 0;
   private Object[] elements;
+
   private Object[] elements = new Object[2];
 
 
 
   public void push(Object element){
 
   public void push(Object element){
 
       assert element != null;
 
       assert element != null;
Строка 146: Строка 136:
 
       elements[size++] = element;
 
       elements[size++] = element;
 
   }
 
   }
  private void ensureCapacity(int capacity) {
+
  private void ensureCapacity(int capacity) {
    if (capacity <= elements.length) {
+
    if (capacity <= elements.length) {
 
         return;
 
         return;
    }
+
    }
    Object[] newElements = new Object[2 * capacity];
+
    Object[] newElements = new Object[2 * capacity];
    for (int i = 0; i < size; i++) {
+
    for (int i = 0; i < size; i++) {
        newElements[i] = elements[i];
+
        newElements[i] = elements[i];
    }
+
    }
  }
+
    elements = newElements;
  public Object pop() {
+
  }
    assert size > 0;
+
  public Object pop() {
    return elements[--size];
+
    assert size > 0;
  }
+
    return elements[--size];
+
  }  
  public int size() {
+
  public int size() {
    return size;
+
    return size;
  }
+
  }
 
+
  public boolean isEmpty() {
  public boolean isEmpty() {
+
    return size == 0;
    return size == 0;
+
  }
  }
+
  public Object peek() {
  public Object peek() {
+
    assert size > 0;
    assert size > 0;
+
    return elements[size - 1];
    return elements[size - 1];
+
  }
  }
 
 
 
 
  }
 
  }
  
Строка 182: Строка 170:
 
Контракты:
 
Контракты:
  
<tex>push </tex>
+
push
 
+
pre: element != NULL  
<tex>pre: element != NULL </tex>
+
post: size = size' + 1  and   elements[size'] == element
 
+
void push (Object  element)  
<tex>post: size = size' + 1</tex> <tex> and </tex> <tex>  elements[size'] == element </tex>
 
 
 
<tex> void</tex> <tex> push (Object</tex> <tex> element) </tex>
 
 
 
 
 
<tex> pop:</tex>
 
 
 
<tex> pre: size > 0 </tex>
 
 
 
<tex>post: size == size' - 1</tex> <tex> and </tex> <tex>result == elements[size]</tex>
 
 
 
<tex> Object</tex> <tex> pop() </tex>
 
 
 
 
 
 
 
<tex> peek:</tex>
 
 
 
<tex>pre: size > 0</tex>
 
 
 
<tex>post: result == elements[size - 1]</tex>
 
 
 
<tex> Object</tex> <tex> peek() </tex>
 
 
 
 
 
<tex> size:</tex>
 
 
 
<tex>post: result == size </tex>
 
 
 
<tex>int</tex> <tex> size()</tex>
 
  
 +
pop
 +
pre: size > 0
 +
post: size == size' - 1 and result == elements[size]
 +
Object pop()
  
<tex>isEmpty:</tex>
+
peek
 +
pre: size > 0
 +
post: result == elements[size - 1]
 +
Object peek()
  
<tex>post: result == size > 0</tex>
+
size
 +
post: result == size  
 +
int size()
  
<tex>boolean</tex> <tex>isEmpty() </tex>
+
isEmpty
 +
post: result == size > 0
 +
boolean isEmpty()

Текущая версия на 19:23, 4 сентября 2022

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

Предусловие

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

Постусловие

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

Инвариант

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

Пример

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

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