例: 配列を用いたリングバッファ

配列を用いたリングバッファは実用でも一般的に使われます。 例えば、典型的なクライアントサーバモデルにおいて、first-in-first-out (FIFO) に従ってサーバが処理するべき複数のクライアントによる要求を保持するためにリングバッファを用いることができます。 それぞれの要求に (決まった範囲から選択することで) 優先度をつける必要がある場合、 特定の優先度の要求を保持するためにそれぞれの優先度にリングバッファを生成することができます。

リングバッファを表現する値のために、次のような線形抽象型 (つまり抽象観型) を宣言してみましょう:

absvtype
cbufObj (a:vt@ype+, m:int, n: int) = ptr

cbufObj のパラメータの性質のいくつかは、次の証明関数を導入することで捕捉できます:

//
prfun
lemma_cbufObj_param
  {a:vt0p}{m,n:int}
  (buf: !cbufObj(a, m, n)): [m>=n; n>=0] void
//

//
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)
//

現在のバッファが空か満杯であるかを判定するのに cbufObj_get_cap と cbufObj_get_size を単純に使うこともできますが、直接的なアプローチがより効率的です。 次の2つの関数テンプレートは、与えられたリングバッファが空であるか満杯であるかを判定します:

//
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)
//

リングバッファの生成と解放を行なう関数はそれぞれ cbufObj_new と cbufObj_free という名前です:

//
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]

次の2つの関数は、与えられたバッファに対する要素の挿入と削除を行ないます。 おそらくこれらはバッファに対して最も頻繁に使われる操作でしょう:

//
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)
//

リングバッファの生成/削除/操作の関数インターフェイス全体を含むファイルは circbuf.sats から入手できます。

抽象型 cbufObj と circbuf.sats で宣言されている関数を実装する簡単で実用的な方法はたくさんあります。 ファイル circbuf.dats では、リングバッファを表現するのに4つのポインタ p_beg, p_end, p_frst, p_last を用いる実装を与えました: p_beg と p_end はそれぞれ下敷にする配列の開始と終了アドレスで、p_frst と p_last はそれぞれ (その配列中の) 占有している部分と空いている部分の開始アドレスです。 この実装の特殊な点は、証明の構築を意識的に避けたプログラミングスタイルであることです。 このスタイルで書かれたコードは型安全が保証されていませんが、正式な証明を構築することが高コストであるような状況下では、このスタイルにも大きな実用上の価値があります。 circbuf.sats で宣言された関数について型安全な実装を得ようと試してみれば、この点において誠実な評価を実感できるはずです。

ファイル circbuf2.dats では、ポインタ p_beg と3つの整数 m, n, f によってリングバッファを表現する別の実装を与えています: p_beg は下敷にする配列の開始位置を指し、m は配列のサイズ (つまりバッファの容量)、n はバッファに現在保存されている要素の数、f は今までにバッファから削除された要素の総数です。 繰り返しますが、この実装でも故意に証明の構築をしていません。