absvtype queue_vtype (a:viewt@ype, n:int) = ptr vtypedef queue (a:vt0p, n:int) = queue_vtype (a, n)宣言された抽象型のフルネームは [queue_vtype] で、別名 [queue] が与えられています。 線形かもしれない型 T と整数 N が与えられたとき、型 [queue(T, N)] は型 T の要素を N 個含むキューを表わします。 型 [queue(T, N)] のキューを存在を考えれば、N が自然数であるべきなのは明らかです。 これは次の関数 (もしくはより正確に証明関数) の型によって捕捉されています:
prfun
lemma_queue_param
{a:vt0p}{n:int} (que: !queue (a, n)): [n >= 0] void
次の関数はサイズ 0 のキューを生成します:
fun{} queue_make_nil {a:vt0p} (): queue (a, 0)
関数テンプレートとして [queue_make_nil] を宣言することで、その定義がコンパイル時にインライン化されることを要求できます。
[queue_make_nil] は小さな本体の関数なので、これは理にかなっているでしょう。
次の関数はサイズ 0 のキューを破棄します (そしてそれが占有していたメモリを解放します):
fun{} queue_free_nil {a:vt0p} (que: queue (a, 0)): void
明確に、与えられたキューが空かどうかテストする必要があります。
そこで、この目的のために次の関数を宣言しましょう:
fun{}
queue_is_empty
{a:vt0p}{n:int} (que: !queue (a, n)): bool (n==0)
同様に、与えられたキューが空でないかどうかテストするために、次の関数を宣言しましょう:
fun{}
queue_isnot_empty
{a:vt0p}{n:int} (que: !queue (a, n)): bool (n > 0)
挿入操作のために、次の関数を宣言します:
fun{a:vt0p}
queue_insert_atend{n:int}
(que: !queue (a, n) >> queue (a, n+1), x: a): void
この構文は、[que] が値渡し (call-by-value) の引数であり、なんらかの型 T と整数 N
においてそのキューの型が [queue(T, N)] から [queue(T, N+1)] に変化することを参照していることを示しています。
明らかに、サイズの増加はキューに挿入された1つの要素によるものです。
デバッグのために、次の関数を宣言しましょう:
fun{a:vt0p}
queue_takeout_atbeg{n:int | n > 0} (que: !queue (a, n) >> queue (a, n-1)): a
この構文は、[que] が値渡し (call-by-value) の引数であり、なんらかの型 T と正の整数 N
においてそのキューの型が [queue(T, N)] から [queue(T, N-1)] に変化することを参照していることを示しています。
明らかに、サイズの減少はキューから削除された1つの要素によるものです。
これで抽象型 [queue_vtype] とそれに関連した関数を実装する準備が整いました。
この実装は n がキュー後方部のサイズであるとき、削除操作は O(n) 時間ですが、挿入操作は常に O(1) 時間であることを保証していることは明確です。 また、もし償却時間的計算量を考えると、挿入操作と削除操作は両方とも O(1) 時間であることはたやすく示すことができます。
ここで、この2つのリストを用いたキューの実装に対する実際のコードを見てみましょう。 メモリリークを回避するために GC が必要な関数的なリストの代わりに、 このコードは (型 [sllist] の) 線形片方向リストを使っていて、メモリの取得/解放を明示的に行ないます。
staload "libats/SATS/sllist.sats" datavtype queue (a:viewt@ype+, n:int) = {f,r:nat | f+r==n} QUEUE of (sllist (a, f), sllist (a, r)) // end of [queue] assume queue_vtype (a, n) = queue (a, n)上記のコードは明確に、キューのサイズがその前方部と後方部の長さの和に等しいことを示しています。
implement{}
queue_make_nil () = QUEUE (sllist_nil (), sllist_nil ())
関数 [queue_make_nil] は、空の前方部と空の後方部から成るサイズ 0 のキューを生成します。
implement{} queue_free_nil (que) = let // val+~QUEUE (f, r) = que // prval () = lemma_sllist_param (f) prval () = lemma_sllist_param (r) // prval () = sllist_free_nil (f) prval () = sllist_free_nil (r) // in // nothing end // end of [queue_free_nil]関数 [queue_free_nil] はサイズ 0 のキューを破棄します。 キュー内の要素は線形型である、つまり要素はリソースを含む可能性があるので、キューは何も要素を持たない時のみ安全に解放することができます。
implement{} queue_is_empty (que) = let val+QUEUE (f, r) = que in if sllist_is_nil (f) then sllist_is_nil (r) else false end // end of [queue_is_empty]もし前方部と後方部の両方が空なら、キューは空です。
implement{} queue_isnot_empty (que) = let val+QUEUE (f, r) = que in if sllist_is_cons (f) then true else sllist_is_cons (r) end // end of [queue_isnot_empty]もしその前方部もしくは後方部が空でないなら、キューは空ではありません。 次に示すように [queue_is_empty] を用いて直接 [queue_isnot_empty] を実装することも可能です:
implement{} queue_isnot_empty (que) = let prval () = lemma_queue_param (que) in not (queue_is_empty (que)) end // end of [queue_isnot_empty]なんらかの N について、型 [bool(N == 0)] の値の否定は型 [bool(N != 0)] になることに注意してください。 [N != 0] が [N > 0] を含むことを示すために [N >= 0] を証明する必要があり、それは [lemma_queue_param] を呼び出すことで成立します。
関数 [queue_insert_atend] と [queue_takeout_atbeg] は次のように実装されます:
implement{a} queue_insert_atend (que, x) = let // val+@QUEUE (f, r) = que val () = r := sllist_cons (x, r) prval () = fold@ (que) // in // nothing end // end of [queue_insert_atend] implement{a} queue_takeout_atbeg (que) = let val+@QUEUE (f, r) = que // val () = lemma_sllist_param (f) val () = lemma_sllist_param (r) // val iscons = sllist_is_cons (f) // in // if iscons then let val x = sllist_uncons (f) prval () = fold@ (que) in x end else let prval () = sllist_free_nil (f) val () = f := sllist_reverse (r) val () = r := sllist_nil {a} () val x = sllist_uncons (f) prval () = fold@ (que) in x end // end of [if] // end // end of [queue_takeout_atbeg]この章の最初で与えられた説明にしたがって、挿入操作と削除操作のコードを理解することは簡単なはずです。
実行可能な実装のために、 上記に示したコード全体とテストコードが queue-sllist2.dats から入手できます。