My favorites | Sign in
Project Home Wiki Issues Source
READ-ONLY: This project has been archived. For more information see this post.
Search
for
  Advanced search   Search tips   Subscriptions
Issue 11: Allow for invariants based on object equality
1 person starred this issue and may be notified of changes. Back to list
Status:  Done
Owner:  nels.bec...@gmail.com
Closed:  Oct 2008


 
Project Member Reported by nels.bec...@gmail.com, Sep 16, 2008
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
This issue is a duplicate/is subsumed by issue 42.
Status: Done

Powered by Google Project Hosting