Инвариант:
hours >= 0 and hours <= 23
<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> возвращенное значение будет являться текущим часом.
int getMinutes()
post: возвращенное значение будет являться текущей минутой.
<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> возвращенное значение будет являться текущей секундой.
void setMinutes(int newMinutes)
pre: 0 <= newMinutes < 60
post: minutes == newMinutes
<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>
==== Решение 1 ====
public class ArrayStack {
private int size= 0; private Object[] elements= new Object[2];
public void push(Object element){
assert element != null;
Контракты:
<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>
pop
pre: size > 0
post: size == size' - 1 and result == elements[size]
Object pop()
<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>
