Evaluation Specification Generation

Specification Inference Evaluation

Spec from verified examplesMethodpostconditionloop invariantinvariantBound related annotations\type-related annotationsChatGPT-4StrongarmEvoSpexDaikon
ensures this.value == 0;Counter()
requires Integer.MIN_VALUE <= initialValueCounter(int)
requires initialValue <= Integer.MAX_VALUECounter(int)
ensures this.value == initialValueCounter(int)
requires Integer.MIN_VALUE <= initialValueincr()
requires this.value < Integer.MAX_VALUEincr()
assignable valueincr()
ensures this.value == \old(this.value) + 1incr()
requires Integer.MIN_VALUE <= this.valueincrByN(int)
requires this.value <= Integer.MAX_VALUE - nincrByN(int)
requires n >= 0incrByN(int)
assignable this.valueincrByN(int)
ensures this.value == \old(this.value) + nincrByN(int)
loop_invariant this.value == \old(this.value) + n - tmpIncrByN(int)
decreases tmpIncrByN(int)
requires Integer.MIN_VALUE + 1 <= this.valuedecr()
requires this.value <= Integer.MAX_VALUEdecr()
assignable this.valuedecr()
ensures this.value == \old(this.value) -1decr()
requires Integer.MIN_VALUE + n <= this.valuedecrByN(int)
requires this.value <= Integer.MAX_VALUEdecrByN(int)
requires n >= 0decrByN(int)
assignable this.valuedecrByN(int)
ensures this.value == \old(this.value) - ndecrByN(int)
loop_invariant this.value == \old(this.value) - tmpdecrByN(int)
decreases n - tmpdecrByN(int)
ensures \result == this.valueget()
pureget()
requires Integer.MIN_VALUE <= nset(int)
requires n <= Integer.MAX_VALUEset(int)
assignable this.valueset(int)
ensures this.value == nset(int)
requires sortedArray != nullsearch(int[], int)
requires 0 < sortedArray.lengthsearch(int[], int)
requires sortedArray.length < Integer.MAX_VALUEsearch(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] == valuesearch(int[], int)
ensures \result == -1 <==> (\forall int i; 0 <= i < sortedArray.length; sortedArray[i] != value)search(int[], int)
puresearch(int[], int)
loop_invariant 0 <= losearch(int[], int)
loop_invariant lo < sortedArray.lengthsearch(int[], int)
loop_invariant 0 <= hisearch(int[], int)
loop_invariant hi < sortedArray.lengthsearch(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] < valuesearch(int[], int)
loop_invariant \forall int i; hi < i < sortedArray.length; value < sortedArray[i]search(int[], int)
loop_decreases hi - losearch(int[], int)
invariant -1 < = sizeArrayList class
invariant size < = Integer.MAX_VALUEArraylist class
invariant list ! = nullArraylist class
invariant size < list.lengthArraylist class
invariant (\forall int; 0 < = i < = size; list[i] ! = null)Arraylist class
invariant 0 < = list.lengthArraylist class
invariant list.length < = Integer.MAX_VALUEArraylist class
ensures size == -1ArrayList()
ensures \fresh(list)ArrayList()
pureArrayList()
ensures \result == sizesize()
puresize()
public normal_behaviorget(int)
requires index > = 0get(int)
requires index < = sizeget(int)
assignable \nothingget(int)
ensures \result == list[index]get(int)
alsoget(int)
public exceptional_behaviorget(int)
requires index < 0 || index > sizeget(int)
assignable \nothingget(int)
signals (IndexOutOfBoundsException) trueget(int)
requires o ! = nullcontains(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)
purecontains(Object)
loop_invariant 0 < = icontains(Object)
loop_invariant i < = size + 1contains(Object)
loop_invariant (\forall int j; 0 < = j < i; list[j] ! = o)contains(Object)
decreases size - icontains(Object)
public normal_behaviorset(int, Object)
requires 0 < = indexset(int, Object)
requires index < = sizeset(int, Object)
requires o ! = nullset(int, Object)
requires \type(Object) <: \elemtype(\typeof(list))set(int, Object)
assignable list[index]set(int, Object)
ensures list[index] == oset(int, Object)
alsoset(int, Object)
public exceptional_behaviorset(int, Object)
requires index < 0 || index > sizeset(int, Object)
assignable \nothingset(int, Object)
signals (IndexOutOfBoundsException) trueset(int, Object)
private normal_behaviorenlarge()
requires list.length < Integer.MAX_VALUEenlarge()
requires \type(Object) <: \elemtype(\typeof(list))enlarge()
assignable listenlarge()
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 < = ienlarge()
loop_invariant i < = size + 1enlarge()
loop_invariant (\forall int j; 0 < = j < i; newList[j] == \pre(list[j])))enlarge()
decreases size - ienlarge()
public normal_behavioradd(Object)
requires size < Integer.MAX_VALUE - 1add(Object)
requires o ! = nulladd(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) + 1add(Object)
ensures list[size] == oadd(Object)
alsoadd(Object)
public exceptional_behavioradd(Object)
requires size == Integer.MAX_VALUE - 1add(Object)
assignable size;add(Object)
signals (IndexOutOfBoundsException) trueadd(Object)
public normal_behaviorremove(Object)
requires o ! = nullremove(Object)
requires size > = 0remove(Object)
requires (\exists int i; 0 < = i < = size; list[i] == oremove(Object)
assignable list[*], sizeremove(Object)
ensures size == \old(size) - 1remove(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)
alsoremove(Object)
public normal_behaviorremove(Object)
requires o ! = nullremove(Object)
requires size > = 0remove(Object)
requires (\forall int i; 0 < = i < = size; list[i] ! = o)remove(Object)
assignable list[*], sizeremove(Object)
ensures size == \old(size)remove(Object)
ensures (\forall int i; 0 < = i < = size; list[i] == \old(list[i]))remove(Object)
alsoremove(Object)
public normal_behaviorremove(Object)
requires size == -1remove(Object)
assignable \nothingremove(Object)
loop_invariant 0 < = iremove(Object)
loop_invariant i < = \old(size) + 1remove(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[*], sizeremove(Object)
decreases size - iremove(Object)
loop_invariant i < = jremove(Object)
loop_invariant j < = sizeremove(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 - jremove(Object)
ensures \result < = = > size == -1isEmpty()
pureisEmpty()