| Issue 11: | Allow for invariants based on object equality | |
| 1 person starred this issue and may be notified of changes. | Back to list |
I'd like to have the following invariant for the ListIterator of my
ConsList:
@ClassStates({@State(name="alive",
inv="immutable(curElement) * immutable(startingPoint)"),
@State(name="HASNEXT",
inv="curElement in NONEMPTY"),
@State(name="END",
inv="curElement in EMPTY")
@State(name="FRONT",
inv="curElement==startingPoint")
@State(name="HASPREV",
inv="curElement != startingPoint")})
But I cannot because PLURAL doesn't let me reason about object pointer
equality.
Oct 8, 2008
Project Member
#1
nels.bec...@gmail.com
Status:
Done
|