| Issue 66: | Sync-or-swim sometimes does not require unpacking when it should | |
| 1 person starred this issue and may be notified of changes. | Back to list |
In this method of the Blocking_queue, sync-or-swim does not require
unpacking even though I believe it should:
@Pures({
@Pure(guarantee="PROTOCOL", requires="STILLOPEN", ensures="STILLOPEN"),
@Pure(guarantee="STRUCTURE", use=Use.FIELDS)
})
public final boolean is_empty()
{
return elements.size() <= 0; }
}
Instead what happens is that it forgets 'this' and the error is that 'this'
is not in the required state on return. This is a big problem and I think I
noticed this in NIMBY as well.
May 20, 2009
Project Member
#1
nels.bec...@gmail.com
Status:
Verified
|