1632
правки
Изменения
м
HOURS hours = newHOURS;
MINUTES minutes = newMINUTES;
SECONDS seconds = newSECONDS;
ПредусловиеИнвариант: (например для getHours) Hours hours >= 0 and hours <= 23 minutes >= 0 and minutes < 60 seconds >= 0 && Hours and seconds < 24.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
getHoursvoid setHours(int newHours){ if (HOURSnewHours <0 ||HOURSnewHours >23)
return HOURS hours = newHours;
return HOURShours = newHours;
<tex>
push </tex>
<tex>pre: element != NULL </tex>
<tex>
post: size = size' + 1</tex> <tex> and </tex> <tex> elements[size'] = element </tex>
<tex> void</tex> <tex> push</tex> <tex> (Object</tex> <tex> element)</tex>
<tex> pop:</tex>
<tex> pre: size > 0 </tex>
<tex>post: size == size' - 1 && 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> push pre: element != NULL post: result size =size' + 1 and elements[size'] = size </tex>= element void push (Object element)
<tex pop pre: size >int 0 post: size == size' - 1 and result == elements[size] Object pop()</tex>
<tex peek pre: size >isEmpty0 post:</tex>result == elements[size - 1] Object peek()
<tex> size post: result == size > 0</tex> int size()
<tex isEmpty post: result == size >0 boolean isEmpty() </tex>
rollbackEdits.php mass rollback
}}
== Пример ==
Необходимо гарантировать, что данный класс будет функции данного класса будут возвращать корректные данные, либо, вообще не будет будут работать. public class Time { intHOURSprivate int hours; intMINUTESprivate int minutes; intSECONDSprivate int seconds; public int getHours();
{
return HOURShours;
}
public int getMinutes();
{
return MINUTESminutes;
}
public int getSeconds()
{
return SECONDSseconds;
}
public void setHours(int newHOURS);
{
}
public void setMinutes(int newMINUTES);
{
}
public void setSeconds(int newSECONDS)
{
}
}
==== Решение 1 ====
Выбрасывать исключение. Имеет недостатки: неочевидность проверки, необходимость писать кучу кода вручную.
throw GREAT_Time_Exception;
}
@Contracted // говорит о том, что класс использует контракты – для отображения в IDE
class Time
{ @Ensures ({“result >= 0”,“result <= 23” }) getHoursvoid setHours(int newHours);
{
}
@Requires ({“newHOURS>= 0”,“newHOURS<= 23” })
@Ensures (“HOURS “hours == newHOURS”)
}
@Requires – буквально означает, «Убедиться, что ДО выполнения подпрограммы («условие выполняется»)» Иначе – бросить исключение.
Здесь мы видим, что, как и в Решение 1, осуществляется проверка пред и пост условий для наших методов. В чем разница? Разница в том, что во втором случае это более наглядно и удобно.
== Пример ==
Рассмотрим стек на массиве. У него есть переменные
<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];
}
}
Инвариант:
Контракты:
