Программирование по контракту
Программирование по контракту обеспечивает проверку предусловий и постусловий при выполнении методов классов, пользовательских функций. Также немаловажную роль в правильности написания функций играют инварианты.
Предусловие
| Определение: |
| Предусловие - должно быть выполнено до исполнения действия. |
Постусловие
| Определение: |
| Постусловие - должно быть выполнено после исполнения действия. |
Инвариант
| Определение: |
| Инвариант - определяет глобальные свойства некоторого класса, которые должны соблюдаться после его создания на протяжении всего времени жизни. |
Пример
Необходимо гарантировать, что функции данного класса будут возвращать корректные данные, либо, вообще не будут работать.
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;
}
}
Инвариант:
Постусловия и предусловия:
возвращенное значение будет являться текущим часом.
возвращенное значение будет являться текущей минутой.
возвращенное значение будет являться текущей секундой.
Решение 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, осуществляется проверка пред и пост условий для наших методов. В чем разница? Разница в том, что во втором случае это более наглядно и удобно.
Пример
Рассмотрим стек на массиве. У него есть переменные
число элементов
массив элементов
Методы:
добавить элемент
удалить элемент
получить элемент на вершине
число элементов
проверка на пустоту
public class ArrayStack {
private int size;
private Object[] elements;
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];
}
}
Инвариант:
Размер не отрицателен,
Элементы заполнены
Контракты:
