Back
import assertion BoundedBuffer.BoundedBuffer.*;
import assertion BoundedBuffer.add.*;
import predicate BoundedBuffer.*;
import predicate BoundedBuffer.add.*;
import predicate BoundedBuffer.take.*;
/**
* Enable PositiveBound pre-cond. assertion of BoundedBuffer
*/
PositiveBoundAndPost: enable assertions { PositiveBound, addPost };
/**
* Indices always stay in range
*/
IndexRange: forall[b:BoundedBuffer].
{IndexRange(b)} is universal globally;
/**
* Full-buffers eventually get emptied
*/
FullToNonFull: forall[b:BoundedBuffer].
{!Full(b)} responds to {Full(b)} globally;
/**
*
*/
NoTakeWhileEmpty: forall[b:BoundedBuffer].
{BoundedBuffer.take.takeReturn(b)} is absent
after {BoundedBuffer.Empty(b)}
until {BoundedBuffer.add.addInvoke(b)};
AbsenceOfTakeWhileEmpty: forall[b:BoundedBuffer].
{BoundedBuffer.take.take(b)} is absent
after {BoundedBuffer.Empty(b)}
until {BoundedBuffer.add.addInvoke(b)};
Back