1632
правки
Изменения
м
<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
pre: 0 <= newMinutes < 60
post: minutes == newMinutes
void setSeconds(int newSeconds)
Контракты:
pop
pre: size > 0
post: size == size' - 1 and result == elements[size]
Object pop()
