Extended Example – Circular Queue
Many of the method contract concepts above are illustrated below with an example of a Circular Queue (i.e., a ring buffer). The example also illustrates additional concepts not yet documented above including invariants, separation of public interfaces (with contracts) from private implementations (with more detailed contracts), spec variables, specification helper methods, and data refinement (relating an public-facing abstract view of a data structure to multiple concrete implementations).
For now, documentation is given in-line in program comments
/*============================================================================
*
* A b s t r a c t R e p r e s e n t a t i o n of Q u e u e
*
*============================================================================*/
/*
Create a trait to serve as the abstract interface for the circular queue.
The trait is parameterized by the type of elements E.
Slang's @record specifier is used to indicate that the trait can be implemented by
an object structure whose fields can be updated.
The queue operations implement a First-In First-Out (FIFO) policy, where new elements
are inserted in the "rear" of the queue and removed from the "front" of the queue.
In the abstract representation (a sequence) for the queue,
the "front" of the queue is the 0th position in the sequence, and
"rear" of the queue is the highest index position of the sequence (max - 1).
*/
@record trait CircularQueue[E] {
/* Define a specification variable to publicly expose the abstract state of the circular queue.
The abstract state is represented by a (M)utable (S)equence indexed by (Z) (type MSZ),
where the front of the queue (first to dequeue) is a the 0th index position.
@spec indicates that the definition will not be presented in the deployed program;
it is introduced for specification and verification/proof purposes only.
The deployed code will have a concrete representation of the queue provided by
a Slang object that implements this trait.
*/
@spec var rep: MSZ[E] = $
/* Define a specification definition to establish properties relating the publicly
exposed abstract state of the queue to it's underlying implementation.
In the scientific literature on contract languages, this is often called the
"representation invariant"/
This will be refined by implementors of the interface/trait to give more about
the relationship between the abstract state and the implementation.
it is introduced for specification and verification/proof purposes only.
*/
@spec def repInv = Invariant(rep.size <= max)
/*----------------------------------
P r o p e t i e s
The following definitions capture the properties of the queue that impact
the queue's behavior. These will be filled in when implementing classes
are developed and instances are created.
*----------------------------------*/
/* The interface exposes the maximum number of elements in the queue.
"@pure" indicates that evaluating this definition produces no visible
side effects.
*/
@pure def max: Z
/* The default value for concrete queue slots that are logically "empty".
* This concept only applies to the concrete
* representation (the notion of empty slots is not manifested in the abstract
* representation since it is a variable length structure that only holds the
* elements that are logically in the queue).
* However, default needs to be exposed in the interface representation
* to make the opportunity to select the default value visible to clients.
*/
@pure def default: E
/* Indicates if the unused positions in the queue are to be overwritten
* with the default value above. This concept only applies to the concrete
* representation.
*/
@pure def scrub: B
/* Indicates the semantics (policy) to be followed when the queue is full and
* there is an attempt to add another element.
*/
@pure def policy: CircularQueue.Policy.Type
/*----------------------------------
O p e r a t i o n s
The following definitions capture the queries and operations on the queue.
At this point, only the method signatures and contracts for the operations
are given. Slang's "Contract.Only" construct is used to provide a contract
without a method implementation.
*----------------------------------*/
// Contract states the returned value should correspond to the size of the
// abstract representation of the queue.
// Size corresponds to the current number of elements in the queue.
def size: Z = Contract.Only(Ensures(Res == rep.size))
// Contract states the returned value should be the result of comparing
// the size of the abstract representation of the queue to zero.
def isEmpty: B = Contract.Only(Ensures(Res == (rep.size == 0)))
// opposite of above
def nonEmpty: B = Contract.Only(Ensures(Res == (rep.size != 0)))
// Contract states the returned value should be the result of comparing
// the size of the abstract representation of the queue to max size of queue.
def isFull: B = Contract.Only(Ensures(Res == (rep.size == max)))
// Enqueue - add an element to the rear of the queue.
// The contract uses Slang's contract cases notation to address three cases:
// - queue is not full
// - queue is full and policy is "drop front"
// - queue is full and policy is "drop rear"
// In all cases, the state of the queue (rep) is being modified
def enqueue(element: E): Unit = Contract.Only(
Modifies(rep),
Case("Non-full",
// Non-full case is selected when size is less than max
Requires(rep.size < max),
// New value (denoted by rep -- the value of rep in the post-state)
// is obtained by adding the element to the end queue as it was
// in the pre-state (denoted by "In(rep)")
Ensures(rep == In(rep) :+ element)
),
Case("Drop front policy and full",
// This case is selected when size = max and the policy is drop front
// i.e., the "oldest" element in the queue is to be dropped
Requires(
policy == CircularQueue.Policy.DropFront,
rep.size == max
),
Ensures(
// The size of rep in the post-state is equal to size of rep in the pre-state
rep.size == In(rep).size,
// All the previous elements of the queue are moved forward one position,
// except for the oldest element at index 0, which is overwritten
All(1 until rep.size)(i => rep(i - 1) == In(rep)(i)),
// The value is inserted at the rear of the queue
rep(rep.size - 1) == element
)
),
Case("Drop rear policy and full",
// This case is selected when size = max and the policy is drop rear
// i.e., the most recent element in the queue is to be dropped
Requires(
policy == CircularQueue.Policy.DropRear,
rep.size == max
),
Ensures(
// The size of rep in the post-state is equal to size of rep in the pre-state
rep.size == In(rep).size,
// Use a "helper predicate" msEqualExcept from ContractUtil
// to state a frame condition that the queue in the pre-state is equal to the
// queue in the post-state except for the element at the rear of the queue, i.e.,
// at index position rep.size - 1
msEqualExcept(rep, In(rep), rep.size - 1),
rep(rep.size - 1) == element
)
)
// TODO: Need to double-check the logic for the Full and NoDrop case.
)
def dequeue(): E = Contract.Only(
// One can only dequeue when there is at least one element in the queue
Requires(rep.size > 0),
// The queue is modified
Modifies(rep),
Ensures(
// dequeueing an element decreases the size by 1
rep.size == In(rep).size - 1,
// all elements other than the one at the front (index 0)
// are moved forward in the queue (note: "until" is non-inclusive on upper bound)
All(1 until In(rep).size)(i => rep(i - 1) == In(rep)(i)),
// Return the element at the front of the queue
Res == In(rep)(0)
)
)
/* elements - defines a method to return all the elements of the queue
* as a mutable sequence. This enables the clients of the queue to get
* all the elements at once without seeing the underlying representation.
* The construction (simplicity) of the contract relies on the design decision
* to present the implementation-independent collection of elements using the
* same type (MSZ[E]) that was used in the contract design to represent the
* abstract value of the queue.
*/
def elements: MSZ[E] = Contract.Only(Ensures(Res == rep))
override def string: String = {
return elements.string
}
}
/*============================================================================
*
* C o n c r e t e R e p r e s e n t a t i o n of Q u e u e
*
*============================================================================*/
object CircularQueue {
/*----------------------------------
H e l p e r D e f i n i t i o n s
*----------------------------------*/
@enum object Policy {
'NoDrop // pre-conditions on enqueue do not allow the value to be inserted when the queue is full
'DropFront // the "oldest" element in the queue is dropped
'DropRear // the most recently inserted element in the queue is dropped
}
/* inv[E]
*
* Defines a boolean helper method that will be used to define the class invariant in
* each of the three classes providing concrete implementations of the circular queue
* (NoDrop, DropFront, and DropRear)
*/
@strictpure def inv[E](max: Z, default: E, scrub: B, queue: MSZ[E], front: Z, rear: Z, numOfElements: Z): B =
max > 0 &
max + 1 == queue.size & // TODO: don't understand this constraint.
// May we always create one extra slot so that rear always
// points to an empty slot (to make the reasoning easier)
queue.isInBound(front) & // uses the isInBound method of the MSZ class to check if front index is in bounds
queue.isInBound(rear) & // ..and the same for rear index
0 <= numOfElements &
numOfElements <= max &
// Establish relationship between numOfElements and front and rear indices, where the
// relationship depends on the relative position of rear, front as they wrap around the
// circular representation.
// TODO: it seems a bit more natural to capture this with an implies
(rear >= front) === (numOfElements == rear - front) &
(rear < front) === (numOfElements == rear + queue.size - front) &
// If the scrub option is set, all the "unused" slots in the queue should be set to
// the default value. Note "modPos" is used to wrap the index position correctly
// in the "circular" concrete representation.
(scrub imply_: All(0 until queue.size - numOfElements)(i => queue(modPos(rear + i, queue.size)) == default))
/* refinement[E]
*
* Defines a boolean helper method that is true is the concrete representation of the queue
* (reflected by the queue, numOfElements, and front parameter) corresponds to the abstract
* representation of the queue (reflected by the rep parameter).
*/
@strictpure def refinement[E](rep: MSZ[E], queue: MSZ[E], numOfElements: Z, front: Z): B =
// number of elements is the same in both representations
rep.size == numOfElements &
// the element at position i in the abstract representation
// matches the value at the "logical" position i in the concrete representation.
// The modPos helper is used to wrap the i correctly back to the low index positions
// of the concrete representation.
//
// modPos(n: Z, m: Z): Z = if (n < m) n else n - m
All(rep.indices)(i => rep(i) == queue(modPos(front + i, queue.size)))
/* refinement[E]
*
* Defines a boolean helper method to use in the post-condition of the create method
* for each kind of queue (NoDrop, DropFront, DropRear). The method ensures that the
* basic attributes of the concrete representation (the "res" parameter) are set correctly.
*/
@strictpure def createEnsures[E](res: CircularQueue[E], max: Z, default: E, scrub: B, policy: Policy.Type): B =
res.max == max &
res.default == default &
res.scrub == scrub &
res.policy == policy
/*----------------------------------------------------------
* NoDrop C o n c r e t e R e p r e s e n t a t i o n
*----------------------------------------------------------*/
object NoDrop {
/* create[E]
*
* Creates a concrete representation of the circular queue that implements the
* NoDrop policy when the queue is full (the method acts as a constructor)
*
*/
@pure def create[E](max: Z, default: E, scrub: B): NoDrop[E] = {
Contract(
Ensures(
// ensure that attributes are correctly set
createEnsures(Res, max, default, scrub, Policy.NoDrop) &
// ensure that state of the concrete representation is appropriately initialized
additionalCreateEnsures(Res) &
// ensure that abstract representation is appropriately initialized
// to the empty sequence
// TODO: seems like it might be nice to have a helper method that is shared
// between all concrete representations to handle this
Res[NoDrop[E]].rep == MSZ[E]()
)
)
// call the constructor for the NoDrop class defined below
// TODO: I don't understand why max + 1 is used
return NoDrop(max, default, scrub, MS.create(max + 1, default), 0, 0, 0)
}
/*
* additionalCreateEnsures[E]
*
* helper spec - specifies that the state of the concrete representation is
*/
// appropriately initialized
@strictpure def additionalCreateEnsures[E](res: NoDrop[E]): B =
res.front == 0 &
res.rear == 0 &
res.numOfElements == 0 &
// Note: isAllMS ensures that all positions of the res.queue have the value res.default
isAllMS(res.queue, res.default)
}
/* Class that conforms to the interface of the CircularQueue trait, and
* provides a queue implementation that implements the NoDrop policy.
*
*/
@record class NoDrop[E](val max: Z,
val default: E,
val scrub: B,
queue: MSZ[E],
// index of oldest element in queue; dequeue always takes the element
// at index front
var front: Z,
// index of next available slot; enqueue always inserts at index rear
// Note: front points to a "used" slot; rear points to an "unused" slot
var rear: Z,
// number of logical elements currently in the queue
var numOfElements: Z) extends CircularQueue[E] {
// defines the class invariant using the inv helper spec defined above.
// The invariant will be automatically included in the pre and post condition
// for each method in the class.
//
// TODO: given that the way that the constructor is defined outside of the class,
// how do we recognize that the invariant should be applied to the post-condition of the
// constructor?
@spec def invariant = Invariant(
inv(max, default, scrub, queue, front, rear, numOfElements)
)
// Formally specify the desired data refinement that relates the
// rep state (abstract) to the queue, front, rear, and numOfElements state (concrete).
// The relationship between these is captured via third item in the DataRefinement
// contract, which is a boolean expression stated using the refinement helper spec
// defined above.
Contract(
DataRefinement(rep)(queue, front, rear, numOfElements)(
refinement(rep, queue, numOfElements, front)
)
)
// provide the concrete implementation of the policy attribute introduced in
// the interface (CircularQueue trait)
@strictpure def policy: Policy.Type = Policy.NoDrop
// provide the concrete implementation of the size method introduced in
// the interface (CircularQueue trait)
override def size: Z = {
// define the contract for the concrete implementation in terms of the concrete
// state. Verification obligations are auto-generated requiring that the interface
// contract is also satified by the method below, and that must be established by
// relying on the refinement relationship between the concrete and abstract state.
Contract(Ensures(Res == numOfElements))
return numOfElements
}
// provide the concrete implementation of the isEmpty method introduced in
// the interface (CircularQueue trait)
override def isEmpty: B = {
Contract(Ensures(Res == (numOfElements == 0)))
return numOfElements == 0
}
// provide the concrete implementation of the nonEmpty method introduced in
// the interface (CircularQueue trait)
override def nonEmpty: B = {
Contract(Ensures(Res == (numOfElements != 0)))
return !isEmpty
}
// provide the concrete implementation of the isFull method introduced in
// the interface (CircularQueue trait)
override def isFull: B = {
Contract(Ensures(Res == (numOfElements == max)))
return numOfElements == max
}
/* enqueue[E]
*
* Provides a concrete implementation of enqueue that realizes the
* NoDrop policy. In effect, the NoDrop policy is achieved by having
* a contract that does not allow the method to be called when the queue
* is full.
*
*/
override def enqueue(element: E): Unit = {
Contract(
// queue is not full
Requires(numOfElements != max),
Modifies(queue, rear, front, numOfElements),
Ensures(
// new value is placed in rear of queue, as indicated by pre-state value of rear
queue(In(rear)) == element,
// update rear, and make sure that it wraps around if necessary
rear == modPos(In(rear) + 1, queue.size),
numOfElements == In(numOfElements) + 1,
// the post-state queue must be the same as the pre-state queue except for the
// value in the rear position
msEqualExcept(queue, In(queue), In(rear))
)
)
queue(rear) = element
rear = modPos(rear + 1, queue.size)
numOfElements = numOfElements + 1
}
/* dequeue[E]
*
* Provides a concrete implementation of dequeue.
*
*/
override def dequeue(): E = {
Contract(
Requires(numOfElements != 0),
Modifies(queue, front, numOfElements),
Ensures(
numOfElements == In(numOfElements) - 1,
front == modPos(In(front) + 1, queue.size),
Res == queue(In(front))
)
// Note: the fact that scrubbing occurs correctly is enforced in the
// post-condition by the automatically included invariant
)
val r = queue(front)
if (scrub) {
queue(front) = default
}
front = modPos(front + 1, queue.size)
numOfElements = numOfElements - 1
return r
}
/* elements MSZ[E]
*
* Provides a concrete implementation of elements.
*
*/
override def elements: MSZ[E] = {
Contract(Ensures(refinement(Res, queue, numOfElements, front)))
val r = MS.create(numOfElements, default)
for (i <- 0 until numOfElements) {
r(i) = queue(modPos(front + i, queue.size))
}
return r
}
}
/*----------------------------------------------------------
* DropFront C o n c r e t e R e p r e s e n t a t i o n
*
* Note: Much of the code for this implementation follows
* the NoDrop implementation, and comments/documentation are
* omitted except where the implementation differs in an
* interesting way
*----------------------------------------------------------*/
object DropFront {
@pure def create[E](max: Z, default: E, scrub: B): DropFront[E] = {
Contract(
Ensures(
createEnsures(Res, max, default, scrub, Policy.NoDrop) &
additionalCreateEnsures(Res) &
Res[DropFront[E]].rep == MSZ[E]()
)
)
return DropFront(max, default, scrub, MS.create(max + 1, default), 0, 0, 0)
}
@strictpure def additionalCreateEnsures[E](res: DropFront[E]): B =
res.front == 0 &
res.rear == 0 &
res.numOfElements == 0 &
isAllMS(res.queue, res.default)
}
@record class DropFront[E](val max: Z,
val default: E,
val scrub: B,
queue: MSZ[E],
var front: Z,
var rear: Z,
var numOfElements: Z) extends CircularQueue[E] {
@spec def invariant = Invariant(
inv(max, default, scrub, queue, front, rear, numOfElements)
)
Contract(
DataRefinement(rep)(queue, front, rear, numOfElements)(
refinement(rep, queue, numOfElements, front)
)
)
@strictpure def policy: Policy.Type = Policy.DropFront
override def size: Z = {
Contract(Ensures(Res == numOfElements))
return numOfElements
}
override def isEmpty: B = {
Contract(Ensures(Res == (numOfElements == 0)))
return numOfElements == 0
}
override def nonEmpty: B = {
Contract(Ensures(Res == (numOfElements != 0)))
return !isEmpty
}
override def isFull: B = {
Contract(Ensures(Res == (numOfElements == max)))
return numOfElements == max
}
override def enqueue(element: E): Unit = {
Contract(
// no pre-conditions; method can be called even when queue is full
Modifies(queue, rear, front, numOfElements),
Ensures(
// new element goes in position of pre-state rear
queue(In(rear)) == element,
// move rear index one position forward, and wrap if necessary
rear == modPos(In(rear) + 1, queue.size),
// update numOfElements for case when the queue was NOT full
(In(numOfElements) < max) === (numOfElements == In(numOfElements) + 1),
// update numOfElements for case when the queue was full
(In(numOfElements) == max) === (numOfElements == In(numOfElements)),
// all elements of the pre-state queue and post-state queue are equal,
// except for the value at In(rear)
msEqualExcept(queue, In(queue), In(rear))
)
)
// if the queue is full, simply call dequeue to remove the front element
if (isFull) {
dequeue()
}
queue(rear) = element
rear = modPos(rear + 1, queue.size)
numOfElements = numOfElements + 1
}
override def dequeue(): E = {
Contract(
Requires(numOfElements != 0),
Modifies(queue, front, numOfElements),
Ensures(
numOfElements == In(numOfElements) - 1,
front == modPos(In(front) + 1, queue.size),
Res == queue(In(front))
)
)
val r = queue(front)
if (scrub) {
queue(front) = default
}
front = modPos(front + 1, queue.size)
numOfElements = numOfElements - 1
return r
}
override def elements: MSZ[E] = {
Contract(Ensures(refinement(Res, queue, numOfElements, front)))
val r = MS.create(numOfElements, default)
for (i <- 0 until numOfElements) {
r(i) = queue(modPos(front + i, queue.size))
}
return r
}
}
/*----------------------------------------------------------
* DropRear C o n c r e t e R e p r e s e n t a t i o n
*
* Note: Much of the code for this implementation follows
* the NoDrop implementation, and comments/documentation are
* omitted except where the implementation differs in an
* interesting way
*----------------------------------------------------------*/
object DropRear {
@pure def create[E](max: Z, default: E, scrub: B): DropRear[E] = {
Contract(
Ensures(
createEnsures(Res, max, default, scrub, Policy.NoDrop) &
additionalCreateEnsures(Res) &
Res[DropRear[E]].rep == MSZ[E]()
)
)
return DropRear(max, default, scrub, MS.create(max + 1, default), 0, 0, 0)
}
@strictpure def additionalCreateEnsures[E](res: DropRear[E]): B =
res.front == 0 &
res.rear == 0 &
res.numOfElements == 0 &
isAllMS(res.queue, res.default)
}
@record class DropRear[E](val max: Z,
val default: E,
val scrub: B,
queue: MSZ[E],
var front: Z,
var rear: Z,
var numOfElements: Z) extends CircularQueue[E] {
@spec def invariant = Invariant(
inv(max, default, scrub, queue, front, rear, numOfElements)
)
Contract(
DataRefinement(rep)(queue, front, rear, numOfElements)(
refinement(rep, queue, numOfElements, front)
)
)
@strictpure def policy: Policy.Type = Policy.DropRear
override def size: Z = {
Contract(Ensures(Res == numOfElements))
return numOfElements
}
override def isEmpty: B = {
Contract(Ensures(Res == (numOfElements == 0)))
return numOfElements == 0
}
override def nonEmpty: B = {
Contract(Ensures(Res == (numOfElements != 0)))
return !isEmpty
}
override def isFull: B = {
Contract(Ensures(Res == (numOfElements == max)))
return numOfElements == max
}
override def enqueue(element: E): Unit = {
// In contrast to enqueue in the other implementations, Contract Cases are used
// to handle the various wrapping scenarios instead of using spec helpers calculating
// the wraps
Contract(
Modifies(queue, rear, front, numOfElements),
Case("Non-full and rear is not the last index",
Requires(
// indicates that we can insert without dropping
In(numOfElements) < max,
// indicates that we don't need to wrap
rear < max
),
// straight-forward calculations, when no dropping and no wrapping
Ensures(
numOfElements == In(numOfElements) + 1,
rear == In(rear) + 1,
queue(In(rear)) == element,
msEqualExcept(queue, In(queue), In(rear))
)
),
Case("Non-full and rear is the last index",
Requires(
// indicates that we can insert without dropping
In(numOfElements) < max,
// indicates that we will have to wrap the update of rear
rear == max
),
Ensures(
numOfElements == In(numOfElements) + 1,
// rear is wrapped
rear == 0,
// TODO: I would rather see the constraints below expressed directly in
// terms of In(rear), since the "invariant" concept is that one always
// inserts at rear when queue is not full.
queue(max) == element,
msEqualExcept(queue, In(queue), max)
)
),
Case("Full and rear is the first index",
Requires(
// when full, we need to insert at the "logical" rear - 1 position,
// overwriting the previous insertion
numOfElements == max,
// ...and when rear == 0, we need to wrap backwards to high-end of the sequence
// to obtain the "physical" index representing the "logical" rear - 1 position
rear == 0
),
Ensures(
// an element is dropped so no increment
numOfElements == In(numOfElements),
// overwriting last inserted value, so no change
rear == In(rear),
// TODO: the way this is spec'ed, the correspondence between max and logical rear - 1
// is a bit unclear. Either put a specific constraint in here that uses modNeg
// or make a reference to the invariant that makes such a relationship clear.
queue(max) == element,
msEqualExcept(queue, In(queue), max)
)
),
Case("Full and rear is not the first index",
Requires(
// when full, we need to insert at the "logical" rear - 1 position,
// overwriting the previous insertion
// TODO: In shouldn't be used below (since this is the precondition)
In(numOfElements) == max,
// rear is greater than 0, so we don't have to wrap backwards
rear > 0
),
Ensures(
// an element is dropped so no increment
numOfElements == In(numOfElements),
// overwriting last inserted value, so no change
rear == In(rear),
// since the queue is full, we insert at rear - 1 (overwriting most recent inserted value)
queue(rear - 1) == element,
// input and output queue values are the same, except at rear - 1
msEqualExcept(queue, In(queue), rear - 1)
)
)
)
if (isFull) {
// if full, insert at logical rear - 1, and we don't need to update indices or
// number of elements since we are overwriting most recently inserted value.
queue(modNeg(rear - 1, queue.size)) = element
} else {
// if not full, insert at rear
queue(rear) = element
// move rear index forward, and wrap if necessary
rear = modPos(rear + 1, queue.size)
// increment number of elements
numOfElements = numOfElements + 1
}
}
override def dequeue(): E = {
Contract(
Requires(numOfElements != 0),
Modifies(queue, front, numOfElements),
Ensures(
numOfElements == In(numOfElements) - 1,
front == modPos(In(front) + 1, queue.size),
Res == queue(In(front))
)
)
val r = queue(front)
if (scrub) {
queue(front) = default
}
front = modPos(front + 1, queue.size)
numOfElements = numOfElements - 1
return r
}
override def elements: MSZ[E] = {
Contract(Ensures(refinement(Res, queue, numOfElements, front)))
val r = MS.create(numOfElements, default)
for (i <- 0 until numOfElements) {
r(i) = queue(modPos(front + i, queue.size))
}
return r
}
}
@pure def create[E](max: Z, default: E, scrub: B, policy: Policy.Type): CircularQueue[E] = {
Contract(Ensures(createEnsures(Res, max, default, scrub, policy)))
policy match {
case Policy.NoDrop => return NoDrop.create(max, default, scrub)
case Policy.DropFront => return DropFront.create(max, default, scrub)
case Policy.DropRear => return DropRear.create(max, default, scrub)
}
}
}