Array-based circular buffers are of common use in practice. For instance, in a typical client/server model, a circular buffer can be employed to hold requests issued by multiple clients that are then processed by the server according to the first-in-first-out (FIFO) policy. In a case where each request needs to be given a priority (chosen from a fixed set), a circular buffer can be created for each priority to hold requests of that particular priority.
Let us declare a linear abstract type (that is, abstract viewtype) as follows for values representing circular buffers:
Such values are considered simple linear objects (as inheritance is not an issue to be dealt with in this setting). Given a viewtype VT and two integers M and N, the viewtype cbufObj(VT, M, N) is for a given buffer of maximal capacity M that currently holds N elements of the type VT.Some properties on the parameters of cbufObj can be captured by introducing the following proof function:
The interface for the following two function templates indicates that they can be called to compute the capacity and current size of a buffer:// fun{a:vt0p} cbufObj_get_cap {m,n:int} (buf: !cbufObj(a, m, n)): size_t(m) // fun{a:vt0p} cbufObj_get_size {m,n:int}(buf: !cbufObj(a, m, n)): size_t(n) //
While it is straightforward to use cbufObj_get_cap and cbufObj_get_size to tell whether a buffer is currently empty or full, a direct approach is likely to be more efficient. The following two function templates check for the emptiness and fullness of a given circular buffer:
// fun{a:vt0p} cbufObj_is_empty {m,n:int}(buf: !cbufObj(a, m, n)): bool(n==0) // fun{a:vt0p} cbufObj_is_full {m,n:int}(buf: !cbufObj(a, m, n)): bool(m==n) //
The functions for creating and destroying circular buffers are named cbufObj_new and cbufObj_free, respectively:
// fun{a:vt0p} cbufObj_new {m:pos}(m: size_t(m)): cbufObj(a, m, 0) // fun cbufObj_free {a:vt0p}{m:int}(buf: cbufObj(a, m, 0)): void //
fun cbufObj_clear {a:t@ype}{m,n:int} (buf: !cbufObj(a, m, n) >> cbufObj(a, m, 0)): void // end of [cbufObj_clear]
The next two functions are for inserting/removing an element into/from a given buffer, which are probably the most frequently used operations on buffers:
// fun{a:vt0p} cbufObj_insert {m,n:int | n < m} ( buf: !cbufObj(a, m, n) >> cbufObj(a, m, n+1), x: a ) : void // end of [cbufObj_insert] // fun{a:vt0p} cbufObj_remove {m,n:int | n > 0} (buf: !cbufObj(a, m, n) >> cbufObj(a, m, n-1)): (a) //
Please find on-line the file circbuf.sats containing the entirety of the interface for functions creating, destroying and manipulating circular buffers.
There are many simple and practical ways to implement the abstract type cbufObj and the functions declared in circbuf.sats. In the file circbuf.dats, I give an implementation that employs four pointers p_beg, p_end, p_frst and p_last to represent a circular buffer: p_beg and p_end are the starting and finishing addresses of the underline array, respectively, and p_frst and p_last are the starting addresses of the occupied and unoccupied segments (in the array), respectively. What is special about this implementation is its employing a style of programming that deliberately eschews the need for proof construction. While code written in this style is not guaranteed to be type-safe, the style can nonetheless be of great practical value in a setting where constructing formal proofs is deemed too costly a requirement to be fully fulfilled. Anyone who tries to give a type-safe implementation for the functions declared in circbuf.sats should likely find some genuine appreciation for this point.
In the file circbuf2.dats, I give another implementation in which a circular buffer is represented as a pointer p_beg plus three integers m, n and f: p_beg points to the starting location of the underline array, m is the size of the array (that is, the capacity of the buffer), n is the number of elements currently stored in the buffer and f is the total number of elements that have so far been removed from the buffer. Again, proof construction is delibrately eschewed in this implementation.