ensures this.value == 0; | Counter() | | | | | | | | | |
requires Integer.MIN_VALUE <= initialValue | Counter(int) | | | | | | | | | |
requires initialValue <= Integer.MAX_VALUE | Counter(int) | | | | | | | | | |
ensures this.value == initialValue | Counter(int) | | | | | | | | | |
requires Integer.MIN_VALUE <= initialValue | incr() | | | | | | | | | |
requires this.value < Integer.MAX_VALUE | incr() | | | | | | | | | |
assignable value | incr() | | | | | | | | | |
ensures this.value == \old(this.value) + 1 | incr() | | | | | | | | | |
requires Integer.MIN_VALUE <= this.value | incrByN(int) | | | | | | | | | |
requires this.value <= Integer.MAX_VALUE - n | incrByN(int) | | | | | | | | | |
requires n >= 0 | incrByN(int) | | | | | | | | | |
assignable this.value | incrByN(int) | | | | | | | | | |
ensures this.value == \old(this.value) + n | incrByN(int) | | | | | | | | | |
loop_invariant this.value == \old(this.value) + n - tmp | IncrByN(int) | | | | | | | | | |
decreases tmp | IncrByN(int) | | | | | | | | | |
requires Integer.MIN_VALUE + 1 <= this.value | decr() | | | | | | | | | |
requires this.value <= Integer.MAX_VALUE | decr() | | | | | | | | | |
assignable this.value | decr() | | | | | | | | | |
ensures this.value == \old(this.value) -1 | decr() | | | | | | | | | |
requires Integer.MIN_VALUE + n <= this.value | decrByN(int) | | | | | | | | | |
requires this.value <= Integer.MAX_VALUE | decrByN(int) | | | | | | | | | |
requires n >= 0 | decrByN(int) | | | | | | | | | |
assignable this.value | decrByN(int) | | | | | | | | | |
ensures this.value == \old(this.value) - n | decrByN(int) | | | | | | | | | |
loop_invariant this.value == \old(this.value) - tmp | decrByN(int) | | | | | | | | | |
decreases n - tmp | decrByN(int) | | | | | | | | | |
ensures \result == this.value | get() | | | | | | | | | |
pure | get() | | | | | | | | | |
requires Integer.MIN_VALUE <= n | set(int) | | | | | | | | | |
requires n <= Integer.MAX_VALUE | set(int) | | | | | | | | | |
assignable this.value | set(int) | | | | | | | | | |
ensures this.value == n | set(int) | | | | | | | | | |
requires sortedArray != null | search(int[], int) | | | | | | | | | |
requires 0 < sortedArray.length | search(int[], int) | | | | | | | | | |
requires sortedArray.length < Integer.MAX_VALUE | search(int[], int) | | | | | | | | | |
requires (\forall int i, j; 0 ≤ i < j < sortedArray.length; sortedArray[i] ≤ sortedArray[j]); | search(int[], int) | | | | | | | | | |
ensures 0 <= \result && \result < sortedArray.length <==> (\exists int i; 0 <= i && i < sortedArray.length; sortedArray[i] == value); | search(int[], int) | | | | | | | | | |
ensures \result != -1 ==> sortedArray[\result] == value | search(int[], int) | | | | | | | | | |
ensures \result == -1 <==> (\forall int i; 0 <= i < sortedArray.length; sortedArray[i] != value) | search(int[], int) | | | | | | | | | |
pure | search(int[], int) | | | | | | | | | |
loop_invariant 0 <= lo | search(int[], int) | | | | | | | | | |
loop_invariant lo < sortedArray.length | search(int[], int) | | | | | | | | | |
loop_invariant 0 <= hi | search(int[], int) | | | | | | | | | |
loop_invariant hi < sortedArray.length | search(int[], int) | | | | | | | | | |
loop_invariant (\exists int i; 0 <= i < sortedArray.length; \old(sortedArray[i]) == value) ==> sortedArray[lo] <= value <= sortedArray[hi] | search(int[], int) | | | | | | | | | |
loop_invariant \forall int i; 0 <= i < lo; sortedArray[i] < value | search(int[], int) | | | | | | | | | |
loop_invariant \forall int i; hi < i < sortedArray.length; value < sortedArray[i] | search(int[], int) | | | | | | | | | |
loop_decreases hi - lo | search(int[], int) | | | | | | | | | |
invariant -1 < = size | ArrayList class | | | | | | | | | |
invariant size < = Integer.MAX_VALUE | Arraylist class | | | | | | | | | |
invariant list ! = null | Arraylist class | | | | | | | | | |
invariant size < list.length | Arraylist class | | | | | | | | | |
invariant (\forall int; 0 < = i < = size; list[i] ! = null) | Arraylist class | | | | | | | | | |
invariant 0 < = list.length | Arraylist class | | | | | | | | | |
invariant list.length < = Integer.MAX_VALUE | Arraylist class | | | | | | | | | |
ensures size == -1 | ArrayList() | | | | | | | | | |
ensures \fresh(list) | ArrayList() | | | | | | | | | |
pure | ArrayList() | | | | | | | | | |
ensures \result == size | size() | | | | | | | | | |
pure | size() | | | | | | | | | |
public normal_behavior | get(int) | | | | | | | | | |
requires index > = 0 | get(int) | | | | | | | | | |
requires index < = size | get(int) | | | | | | | | | |
assignable \nothing | get(int) | | | | | | | | | |
ensures \result == list[index] | get(int) | | | | | | | | | |
also | get(int) | | | | | | | | | |
public exceptional_behavior | get(int) | | | | | | | | | |
requires index < 0 || index > size | get(int) | | | | | | | | | |
assignable \nothing | get(int) | | | | | | | | | |
signals (IndexOutOfBoundsException) true | get(int) | | | | | | | | | |
requires o ! = null | contains(Object) | | | | | | | | | |
ensures !\result < == > size == -1 || (\forall int i; 0 < = i < = size; list[i] ! = o) | contains(Object) | | | | | | | | | |
ensures \result < == > (\exists int i; 0 < = i < = size; list[i] == o) | contains(Object) | | | | | | | | | |
pure | contains(Object) | | | | | | | | | |
loop_invariant 0 < = i | contains(Object) | | | | | | | | | |
loop_invariant i < = size + 1 | contains(Object) | | | | | | | | | |
loop_invariant (\forall int j; 0 < = j < i; list[j] ! = o) | contains(Object) | | | | | | | | | |
decreases size - i | contains(Object) | | | | | | | | | |
public normal_behavior | set(int, Object) | | | | | | | | | |
requires 0 < = index | set(int, Object) | | | | | | | | | |
requires index < = size | set(int, Object) | | | | | | | | | |
requires o ! = null | set(int, Object) | | | | | | | | | |
requires \type(Object) <: \elemtype(\typeof(list)) | set(int, Object) | | | | | | | | | |
assignable list[index] | set(int, Object) | | | | | | | | | |
ensures list[index] == o | set(int, Object) | | | | | | | | | |
also | set(int, Object) | | | | | | | | | |
public exceptional_behavior | set(int, Object) | | | | | | | | | |
requires index < 0 || index > size | set(int, Object) | | | | | | | | | |
assignable \nothing | set(int, Object) | | | | | | | | | |
signals (IndexOutOfBoundsException) true | set(int, Object) | | | | | | | | | |
private normal_behavior | enlarge() | | | | | | | | | |
requires list.length < Integer.MAX_VALUE | enlarge() | | | | | | | | | |
requires \type(Object) <: \elemtype(\typeof(list)) | enlarge() | | | | | | | | | |
assignable list | enlarge() | | | | | | | | | |
ensures \fresh(list) | enlarge() | | | | | | | | | |
ensures \type(Object) <: \elemtype(\typeof(list)) | enlarge() | | | | | | | | | |
ensures (\forall int i; 0 < = i < = size; list[i] == \old(list[i])) | enlarge() | | | | | | | | | |
ensures list.length > \old(list.length) | enlarge() | | | | | | | | | |
loop_invariant 0 < = i | enlarge() | | | | | | | | | |
loop_invariant i < = size + 1 | enlarge() | | | | | | | | | |
loop_invariant (\forall int j; 0 < = j < i; newList[j] == \pre(list[j]))) | enlarge() | | | | | | | | | |
decreases size - i | enlarge() | | | | | | | | | |
public normal_behavior | add(Object) | | | | | | | | | |
requires size < Integer.MAX_VALUE - 1 | add(Object) | | | | | | | | | |
requires o ! = null | add(Object) | | | | | | | | | |
requires \type(Object) <: \elemtype(\typeof(list)) | add(Object) | | | | | | | | | |
assignable size, list, list[*] | add(Object) | | | | | | | | | |
ensures (\forall int i; 0 < = i < = \old(size); list[i] == \old(list[i])) | add(Object) | | | | | | | | | |
ensures size == \old(size) + 1 | add(Object) | | | | | | | | | |
ensures list[size] == o | add(Object) | | | | | | | | | |
also | add(Object) | | | | | | | | | |
public exceptional_behavior | add(Object) | | | | | | | | | |
requires size == Integer.MAX_VALUE - 1 | add(Object) | | | | | | | | | |
assignable size; | add(Object) | | | | | | | | | |
signals (IndexOutOfBoundsException) true | add(Object) | | | | | | | | | |
public normal_behavior | remove(Object) | | | | | | | | | |
requires o ! = null | remove(Object) | | | | | | | | | |
requires size > = 0 | remove(Object) | | | | | | | | | |
requires (\exists int i; 0 < = i < = size; list[i] == o | remove(Object) | | | | | | | | | |
assignable list[*], size | remove(Object) | | | | | | | | | |
ensures size == \old(size) - 1 | remove(Object) | | | | | | | | | |
ensures (\exists int i; 0 < = i < = \old(size); \old(list[i]) == o && (\forall int j; 0 < = j < i; list[j] == \old(list[j])) && (\forall int k; i < = k < = size; list[k] == \old(list[k+1]))) | remove(Object) | | | | | | | | | |
also | remove(Object) | | | | | | | | | |
public normal_behavior | remove(Object) | | | | | | | | | |
requires o ! = null | remove(Object) | | | | | | | | | |
requires size > = 0 | remove(Object) | | | | | | | | | |
requires (\forall int i; 0 < = i < = size; list[i] ! = o) | remove(Object) | | | | | | | | | |
assignable list[*], size | remove(Object) | | | | | | | | | |
ensures size == \old(size) | remove(Object) | | | | | | | | | |
ensures (\forall int i; 0 < = i < = size; list[i] == \old(list[i])) | remove(Object) | | | | | | | | | |
also | remove(Object) | | | | | | | | | |
public normal_behavior | remove(Object) | | | | | | | | | |
requires size == -1 | remove(Object) | | | | | | | | | |
assignable \nothing | remove(Object) | | | | | | | | | |
loop_invariant 0 < = i | remove(Object) | | | | | | | | | |
loop_invariant i < = \old(size) + 1 | remove(Object) | | | | | | | | | |
loop_invariant (\forall int k; 0 < = k < = size; list[k] == \old(list[k])) | remove(Object) | | | | | | | | | |
loop_invariant size == \old(size) | remove(Object) | | | | | | | | | |
loop_invariant (\forall int k; 0 < = k < i; list[k] ! = o) | remove(Object) | | | | | | | | | |
loop_modifies list[*], size | remove(Object) | | | | | | | | | |
decreases size - i | remove(Object) | | | | | | | | | |
loop_invariant i < = j | remove(Object) | | | | | | | | | |
loop_invariant j < = size | remove(Object) | | | | | | | | | |
loop_invariant (\forall int k; 0 < = k < i; list[k] ! = o) | remove(Object) | | | | | | | | | |
loop_invariant (\forall int k; 0 < = k < i; list[k] == \old(list[k]) | remove(Object) | | | | | | | | | |
loop_invariant (\forall int k; i < = k < j; list[k] == \old(list[k+1])) | remove(Object) | | | | | | | | | |
loop_invariant (\forall int k; j < k < = size; list[k] == \old(list[k])) | remove(Object) | | | | | | | | | |
loop_modifies list[j..size] | remove(Object) | | | | | | | | | |
decreases size - j | remove(Object) | | | | | | | | | |
ensures \result < = = > size == -1 | isEmpty() | | | | | | | | | |
pure | isEmpty() | | | | | | | | | |