Loop Invariants for the Loop in Line 186

Dynamate produced the following loop invariants. Invariants in green are proven to be loop invariants by ESC Java. Lines in yellow are not (yet) proven.

Show only proven loop invariants.

Iteration 6

Loop Invariant Status
TLists.eq(elementData, 0, ic, null) verified
TLists.eq(elementData, \old(elementData.length), elementData.length, null) verified
TLists.eq(elementData, \old(size), elementData.length, null) verified
TLists.eq(elementData, \old(size), size, null) verified
TLists.eq(elementData, size, \old(size), null) verified
TLists.eq(elementData, size, elementData.length, null) verified
elementData != null verified
ic <= elementData.length verified
ic >= 0 verified
size <= elementData.length verified
size >= 0 verified
size >= ic verified
modCount >= 1 candidate
modCount >= ic candidate
modCount >= size candidate

Iteration 5

Loop Invariant Status
elementData != null verified
ic <= elementData.length verified
ic >= 0 verified
size <= elementData.length verified
size >= 0 verified
size >= ic verified
modCount >= 1 candidate
modCount >= ic candidate
modCount >= size candidate

Iteration 4

Loop Invariant Status
elementData != null verified
ic <= elementData.length verified
ic >= 0 verified
size <= elementData.length verified
size >= 0 verified
size >= ic verified
modCount >= 1 candidate
modCount >= ic candidate
modCount >= size candidate

Iteration 3

Loop Invariant Status
elementData != null verified
ic <= elementData.length verified
ic >= 0 verified
size <= elementData.length verified
size >= ic verified
modCount != elementData.length-1 candidate
modCount >= ic candidate
modCount >= size candidate
size == 0 || size == 1 || size == 4 candidate

Iteration 2

Loop Invariant Status
elementData != null verified
ic <= elementData.length verified
size <= elementData.length verified
size >= ic verified
elementData.length == 0 || elementData.length == 1 || elementData.length == 10 candidate
ic == 0 || ic == 1 candidate
modCount != elementData.length candidate
modCount != elementData.length-1 candidate
modCount == 1 || modCount == 2 candidate
modCount > ic candidate
modCount > size candidate
size != elementData.length-1 candidate
size == 0 || size == 1 candidate

Iteration 1

Loop Invariant Status
elementData != null verified
(\forall int i; (0 <= i && i <= elementData.length-1) ==> (elementData[i] == elementData[size-1])) candidate
(\forall int i; (0 <= i && i <= elementData.length-1) ==> (elementData[i] == null)) candidate
(elementData.length == 1) && ((\forall int i; (0 <= i && i <= elementData.length-1) ==> (elementData[i] == null))) candidate
elementData.length == 1 candidate
ic == 0 || ic == 1 candidate
modCount == 2 candidate
size == 1 candidate
size == elementData.length candidate

No loop invariants have been found so far.