Alloy によるキューのモデリングと代数的仕様記述

alloy_queue.als

// ************************************
//  連結リストを用いたキューのモデル
// ************************************

module alloy_queue[Value]

// ------------------------------------
//   各要素の定義
// ------------------------------------

// Value を値とするキュー
sig Queue {
    entries : set Entry,  // そのキューに属するエントリの集合
}

// キューが値を格納するための場所
// 一つのキューが同じ値を複数持つ可能性があるため、直接 Value を並べることはできない
sig Entry {
    nextEntry : Entry lone -> Queue,  // 先頭から末尾に向かってポインタを張る
    value     : Value,                // 格納している値
    // 2 個のエントリについて、自分たちを含めそこから後方のエントリで
    // 格納している値の並びが一致する (キューの同値性を定義するのに用いる)
    private tailEq : Entry set -> Queue -> Queue
}

// tailEq の再帰的定義
fact recursiveTailEq {
    all q1, q2 : Queue, e1 : q1.entries, e2 : q2.entries |
        let ne1 = e1.nextEntry.q1, ne2 = e2.nextEntry.q2 |
            e1 -> e2 in tailEq.q1.q2
                iff (e1.value = e2.value and (ne1 = none iff ne2 = none) and
                     ne1 -> ne2 in tailEq.q1.q2)
}

// 各キューに属するエントリは直線的に繋がっている
fact linearlyConnected {
    all q : Queue | let ne = nextEntry.q {
        // q に属するすべてのエントリは連結
        all disj e1, e2 : q.entries | e1 -> e2 in ^ne or e2 -> e1 in ^ne
        // エントリの間の繋がりはサイクルを持たない
        all q : Queue, e : Entry | e not in e.^(nextEntry.q)
        // q に属さないすべてのエントリは他のエントリと連結していない
        all e : Entry - q.entries | e not in ne.Entry + Entry.ne
    }
}

// どのキューにも属さない余分なエントリは存在しない
fact noIsolatedEntries {
    all e : Entry | some q : Queue | e in q.entries
}

// 先頭のエントリを取得する補助関数
private fun front (q : Queue) : Entry {
    { e : q.entries | e not in Entry.nextEntry.q }
}

// 末尾のエントリを取得する補助関数
private fun back (q : Queue) : Entry {
    { e : q.entries | e not in nextEntry.q.Entry }
}


// ------------------------------------
//   エクスポートする関係 / 関数
// ------------------------------------

// キューが空かどうか
pred empty (q : Queue) {
    q.entries = none
}

// ふたつのキューの状態が等しいかどうか
pred equiv (q1, q2 : Queue) {
    empty[q1] iff empty[q2]
    front[q1] -> front[q2] in tailEq.q1.q2
}

// 末尾へのエンキュー : q に v をエンキューすると、キューの状態は q' となる
pred enqueue (q, q' : Queue, v : Value) {
    let b = back[q] {
        some e : Entry | let b = back[q] {
            e.value = v
            e not in q.entries
            q'.entries = q.entries + e
            b != none implies {
                b.nextEntry.q' = e
                e.nextEntry.q' = none
            }
        }
        all e : Entry - b | e.nextEntry.q' = e.nextEntry.q
    }
}

// 先頭からのデキュー : q をデキューすると v が得られ、キューの状態は q' となる
pred dequeue (q, q' : Queue, v : Value) {
    let f = front[q] {
        f.value = v
        q'.entries = q.entries - f
        all e : Entry - f | e.nextEntry.q' = e.nextEntry.q
    }
}

// エンキューした結果のキューの状態を取得
fun enq (q : Queue, v : Value) : Queue {
    { q' : Queue | enqueue[q, q', v] }
}

// デキューして得られる値を取得
fun deq (q : Queue) : Value {
    { v : Value | some q' : Queue | dequeue[q, q', v] }
}

// デキューして得られるキューの状態を取得
fun del (q : Queue) : Queue {
    { q' : Queue | some v : Value | dequeue[q, q', v] }
}

// キューに格納されている値の集合を取得
fun values (q : Queue) : Value {
    q.entries.value
}

// キューに格納されている値の (重複を含んだ) 個数を取得
fun size (q : Queue) : Int {
    #q.entries
}


// ------------------------------------
//   仕様の検証
// ------------------------------------

// eqQueue は同値関係
assert equivIsEquivalence {
    all q : Queue | equiv[q, q]
    all q1, q2 : Queue | equiv[q1, q2] implies equiv[q2, q1]
    all q1, q2, q3 : Queue |
        (equiv[q1, q2] and equiv[q2, q3]) implies equiv[q1, q3]
}

// enq は部分関数的
assert enqIsFunctional {
    all q1, q2, q3 : Queue, v : Value |
        q2 + q3 in enq[q1, v] implies equiv[q2, q3]
}

// deq は部分関数的
assert deqIsFunctional {
    all q : Queue | lone deq[q]
}

// del は部分関数的
assert delIsFunctional {
    all q1, q2, q3 : Queue | q2 + q3 in del[q1] implies equiv[q2, q3]
}

// エンキューした結果は空にならない
assert enqLeadsNonempty {
    all q, q' : Queue, v : Value | enqueue[q, q', v] implies not empty[q]
}

// 空のキューに対してデキューはできない
assert noDeqIfEmpty {
    all q, q' : Queue, v : Value | empty[q] implies not dequeue[q, q', v]
}

// 空のキューに対してエンキューしてデキューすると、エンキューした値が返る
assert deqReturnsEnqValIfEmpty {
    all q1, q2, q3 : Queue, v1, v2 : Value |
        (enqueue[q1, q2, v1] and dequeue[q2, q3, v2] and empty[q1])
            implies v1 = v2
}

// 空のキューに対してエンキューしてデキューすると、キューの状態は元に戻る
assert enqAndDeqAreIdIfEmpty {
    all q1, q2, q3 : Queue, v1, v2 : Value |
        (enqueue[q1, q2, v1] and dequeue[q2, q3, v2] and empty[q1])
            implies equiv[q1, q3]
}

// 空でないキューに対してエンキューしてデキューすると、
// エンキューせずにデキューした場合と同じ値が返る
assert enqAndDeqEqDeqIfNonempty {
    all q1, q2, q3 : Queue, v1, v2, v3 : Value |
        (enqueue[q1, q2, v1] and dequeue[q2, q3, v2] and
         dequeue[q1, q3, v3] and not empty[q1])
            implies v2 = v3
}

// 空でないキューに対して、エンキューしてからデキューした場合と
// デキューしてからエンキューした場合とでは、最終的なキューの状態は同じになる
assert enqAndDeqAreCommIfNonempty {
    all q1, q2, q3, q4, q5 : Queue, v1, v2, v3 : Value |
        (enqueue[q1, q2, v1] and dequeue[q2, q3, v2] and
         dequeue[q1, q4, v3] and enqueue[q4, q5, v1] and not empty[q1])
             implies equiv[q3, q5]
}

check equivIsEquivalence for 3

check enqIsFunctional for 4
check deqIsFunctional for 4
check delIsFunctional for 4

check enqLeadsNonempty for 6
check noDeqIfEmpty     for 6
check enqAndDeqAreIdIfEmpty      for 6
check deqReturnsEnqValIfEmpty    for 6
check enqAndDeqEqDeqIfNonempty   for 6
check enqAndDeqAreCommIfNonempty for 6  // 少し時間がかかる