Evaluation Specification Generation

Specification Inference Evaluation

Spec from verified examples	Method	postcondition	loop invariant	invariant	Bound related annotations	\type-related annotations	ChatGPT-4	Strongarm	EvoSpex	Daikon
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()