1632
правки
Изменения
м
<tex> hours >= 0 </tex> <tex> and</tex> <tex> hours <= 23 </tex>
<tex> minutes >= 0 </tex> <tex> and</tex> <tex> minutes < 60 </tex>
<tex> seconds >= 0 </tex> <tex> and</tex> <tex> seconds < 60 </tex>
<tex> int</tex> <tex> getHours() </tex> post: возвращенное значение будет являться текущим часом.
<tex>post:</tex> возвращенное значение будет являться текущим часом.
<tex>int</tex> <tex> getMinutes() </tex>
<tex> int getSeconds() post:</tex> возвращенное значение будет являться текущей минутойсекундой.
<tex> void setHours(intnewHours) pre: 0 </tex> <tex> getSeconds() = newHours </tex>= 23 post: hours == newHours
<tex>post:</tex> возвращенное значение будет являться текущей секундой.
<tex> void </tex> <tex>setHours(int</tex> <tex> newHours)</tex>
<tex> pre: </tex> <tex>0 <= newHours <= 23</tex> <tex> post: </tex> <tex>hours == newHours</tex> <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>
private void ensureCapacity(int capacity) { if (capacity <= elements.length) {
} 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> 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 (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>
<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</tex> <tex>isEmpty() </tex>
rollbackEdits.php mass rollback
== Пример ==
Необходимо гарантировать, что функции данного класса будут возвращать корректные данные, либо, вообще не будут работать.
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;
Инвариант:
Постусловия и предусловия:
int getMinutes()
post: возвращенное значение будет являться текущей минутой.
void setMinutes(int newMinutes)
pre: 0 <= newMinutes < 60
post: minutes == newMinutes
==== Решение 1 ====
public class ArrayStack {
private int size= 0; private Object[] elements= new Object[2];
public void push(Object element){
assert element != null;
elements[size++] = element;
}
return;
}
Контракты:
pop
pre: size > 0
post: size == size' - 1 and result == elements[size]
Object pop()
