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

Материал из Викиконспекты
Перейти к: навигация, поиск
(Пример)
м (rollbackEdits.php mass rollback)
 
(не показана 31 промежуточная версия 3 участников)
Строка 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;
 
     }
 
     }
 
   }
 
   }
Предусловие: (например для getHours()) hours >= 0 && hours <= 23.
+
Инвариант:  
 +
 
 +
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 ====
 
==== Решение 1 ====
 
Выбрасывать исключение. Имеет недостатки: неочевидность проверки, необходимость писать кучу кода вручную.
 
Выбрасывать исключение. Имеет недостатки: неочевидность проверки, необходимость писать кучу кода вручную.
   int getHours(){
+
   void setHours(int newHours){
         if (this.hours < 0 || this.hours > 23)  
+
         if (newHours < 0 || newHours > 23)  
 
             throw GREAT_Time_Exception;
 
             throw GREAT_Time_Exception;
        return hours;
+
        hours = newHours;
 
   }
 
   }
  
Строка 61: Строка 95:
 
   @Contracted // говорит о том, что класс использует контракты – для отображения в IDE
 
   @Contracted // говорит о том, что класс использует контракты – для отображения в IDE
 
   class Time
 
   class Time
   {
+
   {  
     @Ensures ({“result >= 0”,“result <= 23” })
+
     void setHours(int newHours);
    int getHours();
 
 
     {
 
     {
         return HOURS;
+
         hours = newHours;
 
     }
 
     }
 
     @Requires ({“newHOURS>= 0”,“newHOURS<= 23” })
 
     @Requires ({“newHOURS>= 0”,“newHOURS<= 23” })
     @Ensures (“HOURS == newHOURS”)
+
     @Ensures (“hours == newHOURS”)
 
   }
 
   }
 
@Requires – буквально означает, «Убедиться, что ДО выполнения подпрограммы («условие выполняется»)» Иначе – бросить исключение.
 
@Requires – буквально означает, «Убедиться, что ДО выполнения подпрограммы («условие выполняется»)» Иначе – бросить исключение.
Строка 94: Строка 127:
  
 
<tex> isEmpty - </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];
 +
  }
 +
}
  
 
Инвариант:
 
Инвариант:
Строка 103: Строка 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 push(Object 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 pop() </tex>
 
 
 
 
 
 
 
<tex> peek:</tex>
 
 
 
<tex>pre: size > 0</tex>
 
 
 
<tex>post: result == elements[size - 1]</tex>
 
<tex> Object 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()