Summary: It's not used. Reviewed By: mityal Differential Revision: D19537449 fbshipit-source-id: 505e6b87bmaster
parent
b1eb969635
commit
b948c3e182
@ -1,36 +0,0 @@
|
|||||||
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
|
|
@ -1,19 +0,0 @@
|
|||||||
// A weaker version of InterleavedResponse
|
|
||||||
property InterleavedResponseWeak
|
|
||||||
// vertex names: w = got writer; W = used writer; similarly for s, S
|
|
||||||
message "Incompatible methods for putting data into a response were used."
|
|
||||||
prefix "javax.servlet.ServletResponse"
|
|
||||||
nondet (start)
|
|
||||||
start -> start: *
|
|
||||||
start -> w: W = getWriter(R)
|
|
||||||
start -> s: S = getOutputStream(R)
|
|
||||||
w -> sw: S = getOutputStream(r)
|
|
||||||
s -> sw: W = getWriter(r)
|
|
||||||
w -> W: *(w)
|
|
||||||
sw -> sW: *(w)
|
|
||||||
s -> S: *(s)
|
|
||||||
sw -> Sw: *(s)
|
|
||||||
W -> sW: S = getOutputStream(r)
|
|
||||||
S -> Sw: W = getWriter(r)
|
|
||||||
sW -> error: *(s)
|
|
||||||
Sw -> error: *(w)
|
|
Loading…
Reference in new issue