AlloyでIteratorパターンをスケッチ

Alloyという、システムの構造や振る舞いを数学的に記述して、設計の矛盾やバグを検証するための軽量な形式手法言語・ツールがあります。
UMLとかER図の代替みたいにAlloyを利用している記事をよく見かけるが、本質的にAlloyはシステムの構造・振る舞いを論理と関係で記述して、ソフトウェアを設計したり検証したりするものです。
Alloyでソフトウェアを設計するとSATソルバが容赦なく設計のバグ（反例）を暴いてくれるので、Alloyでバグ（反例）が無くなった設計を実際にコードに落とすと、設計に起因するバグはなくなるという代物です。
Alloyで反例がなくなれば、コーディング前にバグなく動くことがわかってしまうというものです。
実際にAlloyで設計して、コーディングするということも日常的に行っているが、その話はまた次回にして、今回はAlloyでデザインパターンをスケッチして、デザインパターンの論理を考えてみようという企画の第一弾。

デザインパターンというと、JavaやC#で使うものというイメージがありますが、Alloyを使えばでデザインパターンの論理モデルを書くことができます。
今回はIteratorパターン。

以下Iteratorパターンの簡単なスケッチです。
今回はCollectionとIteratorでmoduleを分けています。

//
// Collection
//
module behavioral/iterator/Collection[E]

sig Collection {
    items: seq E
}

pred contains [c: Collection, e: E] {
    some i: c.items.inds | c.items[i] = e
}

pred append [c1, c2: Collection, e: E] {
    not contains[c1, e]

    contains[c2, e]
}

assert append_after_contains_true {
    all c1, c2: Collection, e: E |
        append[c1, c2, e] => contains[c2, e]
}
check append_after_contains_true for 6

//
// Iterator
//
module behavioral/iterator/iterator[E]

open behavioral/iterator/Collection[E]

sig Iterator {
    target: one Collection,
    index: one Int
}

pred has_next [it: Iterator] {
    it.index >= 0 and it.index < #it.target.items
}

pred next [it1, it2: Iterator, elem: E] {
    has_next[it1]

    elem = it1.target.items[it1.index]
    it2.target = it1.target
    it2.index = it1.index + 1
}

assert next_returns_valid_element {
    all it1, it2: Iterator, e: E |
        next[it1, it2, e] => {
            e in it1.target.items.elems
            it2.index = it1.index + 1
        }
}
check next_returns_valid_element for 6

今回書いたIteratorパータンはとても小さなモデルで、実質CollectionとIteratorの関係とIteratorのnextの論理と簡単な検証だけしています。

Alloyでは論理しか書けないので、具体的処理のようなものは一切かいていませんが、JavaやC#のクラスを見ているような感じに見えますよね。

今回具体的なコード解説はしませんが、興味のある方はAlloyについて調べてみてください。
Alloyのサイトのリンクを張っておきます。