1632
правки
Изменения
м
<tex>Необходимо гарантировать, что функции данного класса будут возвращать корректные данные, либо, вообще не будут работать. public class Time{{ private int hours; private int minutes; intHOURSprivate int seconds; intMINUTESpublic int getHours(); intSECONDS{ return hours; } getHourspublic int getMinutes();
returnHOURSreturn minutes;
getMinutespublic int getSeconds();
getSecondspublic void setHours(int newHOURS);
return SECONDShours = newHOURS;
setHourspublic void setMinutes(newHOURSint newMINUTES);
HOURS minutes = newHOURSnewMINUTES;
setMinutespublic void setSeconds(newMINUTESint newSECONDS);
MINUTES seconds = newMINUTESnewSECONDS;
SECONDS hours = newSECONDSnewHours;
rollbackEdits.php mass rollback
}}
== Пример ==
{
}
{
return MINUTESseconds;
}
{
}
{
}
{
}
}Инвариант: 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 { setSecondsvoid setHours(newSECONDSint 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()
