infer_clone/infer/tests/codetoanalyze/java/topl/iterators.topl

property HasNext
  prefix "Iterator"
  prefix "List"
  nondet (start)
  start -> start: *
  start -> invalid: I = iterator(*)
  invalid -> valid: <true> = hasNext(i) // treat as shorthand for <B> = hasNext if (b)
  valid -> invalid: next(i)
  invalid -> error: next(i)

property UnsafeIterator
  prefix "Collection"
  prefix "Iterator"
  nondet (start)
  start -> start: *
  start -> iterating: I = iterator(C)
  iterating -> modified: remove(c, *)
  iterating -> modified: add(c, *)
  modified -> error: next(i)

property UnsafeMapIterator
  nondet (start)
  start -> start: *
  start -> gotView: View = keySet(M)
  start -> gotView: View = values(M)
  gotView -> iterating: I = iterator(view)
  iterating -> updated: put(m, *)
  updated -> error: next(i)

property SkipIndexAfterRemove
  prefix "ArrayList"
  nondet (start)
  start -> start: *
  start -> removed: remove(Collection, Index)
  removed -> ok:    get(collection, index)
  removed -> error: get(collection, J) if J != index