プロパティベーステストの前にモデルを Alloy で検証する

正確には「検査」と書くべきですが、本記事では馴染みのある「検証」を基本的に使います。

プロパティベーステストが注目されていますね。私も年末に 『実践プロパティベーステスト ― PropErとErlang/Elixirではじめよう』 を読んでいました。

この本の 10 章では、プロパティベーステストのケーススタディとして書籍の貸し出しシステムの例が扱われています。テストを実装する前に、まずは状態のモデル化を行い、システムに対するすべての操作を挙げています (260 ページ) 。そのうちの一つを抜粋します。

• 「まだシステムに登録されていない本を追加する」に期待されるのは「成功」

同様に、他の操作にも「操作内容」と「期待される結果」が書かれています。これらの仕様を読んでいると、いくつか気にかかることがありました。

• その操作の結果は、他の操作にどのような影響を与えるのか？
• その操作の結果は、他の操作の結果と矛盾しないのか？

これらは、自分で仕様書を読んで理解しなければなりません。いまは AI に頼る手もありますが、それはさておき、人間様が仕様を理解しないでいいわけにはいきません。仕様が膨らむほどコストが高い作業になります。私は個人的な諸々の事情で仕様を覚えたり把握するのがすっかり難しくなってしまいましたので、自虐でも冗談でもなく切実な問題です。

コストが高くつく原因の一つは、仕様が自然言語 (日本語) で書かれているからです。自然言語は曖昧なので、どんなに論理的に書かれた文章であっても、著者の意図を完全に汲み取るのは難しくなります。その上で、他の仕様と検証するにも人力で行う必要があります。前述の通り、いまは AI に頼る手もありますが、 AI が出力するのも自然言語であれば同じことです。

モデルを検証する？

何があれば楽になるのか？ 自分の状況を考えると、

• 仕様の記述に向くテキストベースの厳密な記法
• 人間に変わって検証してくれる機能

があるとよさそうです。特に検証機能があれば、自然言語で考えるコストを減らすことができます。

検証機能とは、仕様に矛盾がないかとか、特定の状況で仕様をどのように解釈すべきなのか、などの疑問をコンピューターに検証させる機能です。ただし、 AI は間違える可能性があるので信頼できる手段ではありません。

そこで試したいのが、 自動検証可能な形式仕様記述言語 (formal specification language) です。なにやら仰々しくて難しそうですが、実は意外と身近な概念だったりします。

「形式」とは、特定の厳密なルールに従う方法や手順です。身近な例だと正規表現が形式言語です。テキストにマッチするパターンを特定のルールに従って表します。もうお気づきかと思いますが、プログラミング言語も形式言語です。

「仕様記述言語」とは、その名の通り仕様を記述するための言語です。身近な例だと UML が仕様記述言語です (厳密な記法もあるので形式言語でもあります) 。 UML は自動検証機能がないので、自分の状況に向きません。

これらの条件を満たす言語として、今回は Alloy を試してみたいと思います。 Alloy はモデル検査のための仕様記述言語であり、解析ツールがセットで配布されています。

モデル検査は数学的な理論 (数理論理学) を基盤としますが、 Alloy は数学を意識しなくてもそれなりに使えます (私も全然知りません) 。この記事を読んで、 Alloy やモデル検査を少しでも身近に感じてもらえたら嬉しいです。

検証するモデル

本記事では、書籍の貸し出しシステムのモデルを Alloy で検査するコードを実装します。このモデルは、『実践プロパティベーステスト』の 10 章で扱われているものです。
ただし、「実践プロパティベーステスト」が手元になくても問題ありません。このモデルは小さいので、記事内で完結します。

Alloy のインストール

Alloy は 公式サイトからダウンロード できます。 macOS なら Homebrew でも次のコマンドでインストールできます (デスクトップアプリが /Applications にインストールされます) 。

brew install alloy

Alloy のアプリケーションは簡易的なエディターを備えていますが、 VSCode の拡張機能 もおすすめです。この拡張機能では、実行可能なコードの上に実行ボタンが表示され、実行結果が VSCode のウィンドウ内で表示されます。

オブジェクトを定義する

最初に、モデルの中心となるオブジェクトを定義します。 Alloy を起動し (VSCode プラグインなら起動は不要です) 、以下の内容のファイルを作成してください。

Bookstore.als:

sig Title {}

sig Author {}

sig Isbn {}

sig Book {
    title: Title,
    author: Author,
    isbn: Isbn,
}

sig NAME {...} は シグネチャ signature と呼び、新しい型を定義する構文です。プログラミング言語でのクラスや構造体の定義に近いです。シグネチャで定義されたモデルは アトム atom と呼ばれます。

シグネチャは複数のフィールドを定義できます。これもプログラミング言語のフィールドやプロパティとだいたい同じです。 Title, Author, Isbn はフィールドを持ちません (定義すべきフィールドがなければ空でも問題ありません) 。 Book は title, author, isbn の 3 つのフィールドを持ちます。 : を挟んで右側がフィールドの型を表します。

文字列型は存在しない

Title, Author, Isbn のシグネチャにフィールドはありません。実際の実装ではこれらのフィールドは文字列型になるでしょうから、 Book の各フィールドの型を String と書きたくなります。しかし、 Alloy に文字列型は存在しません。

文字列型は、プログラミング言語に依存する具体的なデータ型です。言語によっては、文字列専用の型が用意されていない場合もあります。たとえば、「実践プロパティベーステスト」で使われる Erlang には文字列型がありません。便宜的に string という型はありますが、「文字コード (整数) のリスト」の別名です。 Alloy では具体的なデータ型よりも抽象的なデータ型でモデルを表現します。

抽象的に表現するために、もっと具体的なデータを考えてみます。タイトル、著者名、 ISBN をまとめて文字列型で実装するとしても、すべての文字が使えるわけではないでしょう。もしタイトルや著者名に 北海道異体文字 が含まれていたら、割り当てのない Unicode では対応できません。他にも Unicode で表せない文字はいくらでもあります。 ISBN も同様に、 10 桁または 13 桁の数字以外の文字列は不正になります。

これらにもう少し正確な型をつけるとすると、タイトルは「『タイトルに使える文字』のリスト (順序付き集合) 」と考えられます。著者名と ISBN も同様です。 Alloy で定義するならこんな感じでしょうか:

sig TitleCharacter {}

sig Title {
    contents: set TitleCharacter,
}

これで文字列型が不要になりました。もしくは、文字列を表すシグネチャを定義して継承しても (サブタイプを定義する) してもいいかもしれません。以下のようにすると、 Title, Author, Isbn の共通の型 String を用意できます。

sig String {}
sig Title extends String {}
sig Author extends String {}
sig Isbn extends String {}

抽象的なシグネチャになりましたね。

ただ、今回のモデルではそこまで詳細な型が必要ないので扱いません。公文書や古文書を扱うシステムなら、さらなる詳細な型を定義するメリットがあるかもしれません。

システムを定義する

次に、本の在庫管理を行うシステムのシグネチャを定義します。 // で始まる行はコメントです。

sig System {
    // 登録された本
    catalog: set Book,

    // 在庫
    copies: catalog -> Int
}

System シグネチャは、登録された本 catalog と在庫 copies を表す 2 つのフィールドを持ちます。どちらのフィールドの型も見慣れないかと思います。

まず set Book です。 set は多重度を表すキーワードで、 set は順序なしの集合を表します。プログラミング言語の Bag です。 (順序つき集合を扱うには util/ordering モジュールを使います。本記事では割愛します)

次に catalog -> Int です。 catalog はフィールドの catalog を表し、 -> は型の対応付けを表します。プログラミング言語の Map や Dictionary に近いです。

ただし、この catalog はあくまで型を表すだけで、 catalog の内容との関係を示す定義ではないので注意してください。たとえば、 catalog に含まれる Book が copies に含まれることを表すものではありません。

このシグネチャをプログラミング言語の疑似コードで表すと、次のようになります。

sig System {
    catalog: Bag<Book>,
    copies: Map<Book, Int>
}

「本を追加する」操作を定義する

以上でオブジェクトの型を定義しました。ただ、型を定義しただけではまだ何もできません。ここからは、モデルを検証するための要素を定義していきます。

モデルの検証には 制約 constraints が必要です。制約とは、モデルが満たすべき条件やルールです。それは動的な振るまいを表す 操作 operation の定義でも同様です。操作という用語を区別するため、以降は書籍貸出システムに対する操作を「システム操作」、 Alloy の操作を「操作」と呼びます。

まずは「本を追加する」操作を定義します。システム操作と期待される結果を引用します:

• 「まだシステムに登録されていない本を追加する」に期待されるのは「成功」
• 「すでにシステムに登録されている本を追加する」に期待されるのは「失敗」

これらのルールを持つ操作を表すために、今回は 述語 predicate を定義します。述語は特定の条件やルールを満たすかどうかを検証します。引数を持ち、検証結果を真偽値で扱えるので関数に似ていますが、データの加工手段ではありません。プログラミング言語で言うと、例外を投げる assert() みたいな感じです。

Alloy では成否を表す具体的なデータ型はありませんので、今回は状態変化の有無で成否を判断するとします。成功したらシステムに本が追加されるという状態変化があり、失敗したらシステムの状態は何も変わりません。

では、「本を追加する」操作を表す述語 addBook を次のように定義します:

pred addBook [sys: System, sys": System, b: Book] {
    b not in sys.catalog => sys".catalog = sys.catalog + b
}

見慣れない文法に面食らうかもしれません。一つずつ見ていきましょう。

pred は述語の定義を開始するキーワードです。 pred の次に述語名 addBook を指定します。

続く [...] は述語の引数です。各引数は 引数名: 型 の形で宣言します。引数名には " も使えます。 " に特別な意味はなく、 sys" は普通の引数名です。

System が 2 つありますが、 addBook では 1 つ目の引数を「状態変化前 (事前状態) 」、 2 つ目の引数を「状態変化後 (事後状態) 」を表すのに使います。なぜ未来の結果のはずの「状態変化後」があるのかというと、 Alloy の操作は手続き的ではなく 宣言的 だからです。

一般的なプログラミング言語では、データを加工する手順を指定して期待する結果を得ます。 Alloy では、期待する結果を直接的に指定します。述語の内容を見ていきましょう:

b not in sys.catalog => sys".catalog = sys.catalog + b

この式は左辺と右辺に分割できます。 左辺が b not in sys.catalog で、右辺が sys".catalog = sys.catalog + b です。

左辺の A not in B は、オブジェクトの集合 B に A が含まれていないことを表す演算子です。 b not in sys.catalog は、「状態変化前の catalog に b が含まれていない」という意味になります。

両辺をつなぐ => 演算子は、両辺の論理的な関係を表します。後述します。

それを説明する前に、右辺 sys".catalog = sys.catalog + b に進みます。 sys.catalog + b は Book の集合に b を追加します。本の登録を表します。

= は等価演算子です。プログラミング言語で言うと == で、代入ではありません。左辺の sys" は「状態変化後」を表すので、 sys".catalog = sys.catalog + b は「状態変化後の catalog は、状態変化前の catalog に b を追加したものと等しい」ことを表します。

=> 演算子

先程の => 演算子は 含意 implication と言い、「左辺が真ならば右辺も真」という意味です。プログラミング言語で言うと if 文に近いですが、左辺が偽の場合の結果が異なるため同等ではありません。

=> の左辺が偽の場合、 右辺の真偽に関わらず、全体の結果は真 になります。以下に表を示します。

A	B	A => B
真	真	真
真	偽	偽
偽	真	真
偽	偽	真

述語の結果が真であれば、検証結果に問題ないとみなされます。左辺 b not in sys.catalog であれば、システムに本が追加されていれば偽となりますが、 addBook 全体の結果は真となります。また、左辺が偽であれば右辺は評価されないので、 sys".catalog = sys.catalog + b は実行されません。それぞれの結果を表にまとめると以下のようになります:

b not in sys.catalog	sys".catalog = sys.catalog + b	addBook	システムの状態
本は未登録である	本を追加する	真	変化する
本は未登録である	本を追加できない	偽	変化しない
本は登録済み	(評価されない)	真	変化しない
本は登録済み	(評価されない)	真	変化しない

システムの状態が変化するのは「本が未登録かつ追加できた」場合のみになります。システムの仕様では「本が登録済み」であれば失敗とみなすので、本が登録済みのときの addBook の結果が真になるのには違和感があるかもしれません。しかし、システム操作での「失敗」はバグではありません。仕様です。

検証が失敗するのは「本が未登録かつ追加できなかった」場合のみです。追加処理に相当する sys".catalog = sys.catalog + b は単純な操作なので問題なさそうに見えますが、常に成立するとは限りません (後述します) 。

したがって検証結果に問題なければ、「本が未登録」が真であれば「本を追加できる」も 必ず 真となります。これは「本が未登録かつ追加できない」場合の仕様が 他の制約と矛盾がある 、もしくは 未定義 であることも意味します。

含意のあるプログラミング言語は少ない (VBA くらい？) ので飲み込みにくいかもしれませんが、最初のうちは if と同じ感覚で使ってもあまり問題にならないと思います。

なお、 => 演算子は implies キーワードでも表せます。 => が短縮版、 implies が冗長版です。 => と implies のいずれも else と組み合わせられるので、 else を使う場合は見た目を合わせるために implies を使う場合もあります。

モデルを検証する

それでは、 addBook を使って「本を追加する」操作を検証してみましょう。この操作の内容と期待される結果を再び引用します:

• 「まだシステムに登録されていない本を追加する」に期待されるのは「成功」
• 「すでにシステムに登録されている本を追加する」に期待されるのは「失敗」

前節で述べた通り、この場合の失敗はバグではなく仕様です。今回は addBook による「状態の変化」を比較します。検証内容は以下の通りです:

• 「まだシステムに登録されていない本を追加する」に期待されるのは「状態変化あり」かつ「状態変化後に本が追加されている」
• 「すでにシステムに登録されている本を追加する」に期待されるのは「状態変化なし」

検証は アサーション assertion と チェック check コマンドで行います。アサーションで検証内容を定義し、チェックコマンドでアサーションに基づく検証を行います。

今回は、本の追加の成功と失敗を表すアサーションを 2 つに分けて用意します。

• addNewBookSuccess: 未登録の本を追加する。状態変化あり
• addExistingBookFail: 登録済みの本を追加する。状態変化なし

以下に定義を示します。どちらもほぼ同じなのでまとめて示します:

assert addNewBookSuccess {
    all sys, sys": System, b: Book |
        b not in sys.catalog
        implies addBook[sys, sys", b]
        implies b in sys".catalog
}

assert addExistingBookFail {
    all sys, sys": System, b: Book |
        b in sys.catalog
    	    implies addBook[sys, sys", b]
        implies b in sys".catalog
}

アサーションは assert で始め、 {...} に制約を記述します。上記のアサーションでは、 all からブロックの最後までがひとかたまりの式になります。こちらも見慣れない文法なので分解しましょう。

この式は、 (束縛) 変数 sys, sys", b の組み合わせに対する制約を | 演算子で区切って定義します。先頭の all は多重度を表す量指定子の一つで、すべてのインスタンスに対する制約を表します。実行時は考えられる範囲であらゆる内容のインスタンスが生成され、すべての組み合わせが制約を満たすかどうか検証されます。

ついでに他の量指定子も挙げておきます。量指定子はシグネチャなど他の要素でも使います:

• lone: 0 または 1
• one: 1
• some: 1 以上
• no: 0

sys" は、 addBook で触れたようにシステムの「状態変化後」を表すために使います。

b [not] in sys.catalog implies ... implies もひとかたまりの式です。 b [not] in sys.catalog は addBook で定義した式と同じです。 implies は => の冗長表記です。読みやすくするためなのか、アサーションでは implies が使われることが多いようです。

b [not] in sys.catalog が真であれば、 addBook[sys, sys", b] も真であり、式全体が真になります。 => の節で述べた通り、 3 つのうちいずれかの式のみが真になる状況はありません。「すべてが真になる」か「すべてが偽になる」のどちらかになります。

addBook[sys, sys", b] は述語 addBook を制約として指定します。本が未登録であれば addBook で sys".catalog に本が追加されます。最後に b [not] in sys".catalog で、 sys".catalog に本が追加されているかどうかを指定します。

最後の b in sys".catalog は両方のアサーションで同じです。 addExistingBookFail では、本が登録済みの場合に失敗になっても catalog の内容に変化がないことを保証します。当然と言えば当然ですが、当然のことを積み重ねるのが大事です。地道な定義によって想定外のエラーや矛盾を防げます。

アサーションを定義したら、 check コマンドの実行内容を記述します:

check addNewBookSuccess for 5

check addExistingBookFail for 5

check コマンドはアサーションに基づいて検証を行います。 for に続く数値は スコープ scope と呼び、考慮するケースの多さ (範囲) を指定します。スコープについては後述するので、ひとまず実行してみましょう。

デスクトップ版であればメニューの Execute から "Check addNewBookSuccess for 5" を選択します。 VSCode であれば、 check コマンドの行の上にある Execute ボタンを押すと実行できます。

デスクトップ版

VSCode

実行すると、ウィンドウ右側に検証結果が表示されます。

デスクトップ版

VSCode

"No counterexample found. Assertion may be valid." と表示されれば、検証結果に問題ありません。制約がすべて真になることを 妥当 valid と呼びます。

counterexample は 反例 と言い、制約が成立しないケースを指します。その逆の、制約が成立するケースは 充足例 example と呼びます。今回は反例が見つからなかったので、検証結果は妥当です。

インスタンスとスコープ

アサーションはどのように検証されるのか？ Alloy はシグネチャのオブジェクトを生成し、具体例として検証に使います。このオブジェクトを インスタンス instance と呼びます。

インスタンスは、調べるべきあらゆる可能性の関係 (状態や構成) が制約に基づいて生成されます。主な関係を以下に示します:

• 多重度
  型の多重度を網羅します。

  たとえば、 Book.title フィールドの型がもし lone Title であれば、 Book は 0 または 1 つの Title を持ちます。この場合、 Book のインスタンスは 0 つの Title を持つものと 1 つの Title を持つものが生成されます。

  set のような無限の要素を持つ集合型は、一定の数の要素を持つインスタンスが生成されます。 set Int であれば、たとえば 0 から 10 までの整数を持つインスタンスが生成されます。生成される整数の範囲は、制約やスコープによって変わります。

• シグネチャとフィールド
  フィールドの多重度が取り得る組み合わせでシグネチャのオブジェクトを生成します。

  たとえば、 Book.title フィールドと Book.author フィールドの多重度がどちらも lone であれば、 title と author の組み合わせは (0, 0), (0, 1), (1, 0), (1, 1) の 4 通りがあります。この 4 通りの Book インスタンスが生成されます。

  すべてのフィールドの多重度が 1 だったり、またはフィールドが空であれば、シグネチャのオブジェクトは 1 つのインスタンスのみになります。

• シグネチャ間の関係
  シグネチャ同士が取り得る関係を網羅します。

  たとえば、異なる Book インスタンス間で同一の Title を共有するケースがあります。 addBook では Book.title の値を他のインスタンスと共有してはならないという制約はありません。

  また、 System.catalog に追加した Book が System.copied のキーに必ず含まれるという制約もありません。逆に、 copied のキーに含まれる Book が catalog に必ず含まれるという制約もありません。そのため、「 catalog と copied の両方に同じ Book を含む」、「 copied に含まれない Book を catalog が含む」、「 catalog に含まれない Book を copied が含む」などの組み合わせのインスタンスが生成されます。

ただ、シグネチャやフィールドが増えれば増えるほど、関係の組み合わせも劇的に増えます。それらの組み合わせの範囲を決めるのが スコープ scope です。スコープを小さくすればインスタンスの数も少なくなり、スコープを大きくすればインスタンスの数も劇的に増えます。インスタンスが増えれば増えるほど反例を見つけやすくなりますが、あまりスコープを広げると実行が終わりません。

スコープの範囲のメリットとデメリットを挙げます:

範囲	メリット	デメリット
小さい	インスタンスが単純でわかりやすい	反例を見つけにくい
大きい	反例を見つけやすい	インスタンスが複雑でわかりにくい

スコープが大きいと関係の組み合わせがより多様になるので、反例が見つかったときのインスタンスの内容が思いもよらないケースになってしまい、デバッグが難しくなります。そのため最初は小さなスコープから始めて、徐々にスコープを大きくするのが推奨されています。最終的にはスコープが 10 あれば十分なケースを網羅できるようです。

ファクト

述語のような特定の状況における制約に対して、常に成立する制約を ファクト (事実) fact と呼びます。ファクトは述語の実行前と実行後にも適用されるので、もし addBook の実行前に矛盾するファクトがあれば、インスタンスは生成されなくなります。実行後に矛盾するファクトがあれば、反例が見つかったとみなされます。

ファクトを定義する前に、実際に生成されるインスタンスを見てみましょう。以下のコマンドを記述してください:

run addBook

run コマンドは、指定した制約を満たすインスタンスを探します。こちらも check と同じく Execute メニューから実行できます。実行すると、次のようなウィンドウが開きます (VSCode の場合は、実行後に "Instance found. Predicate is consistent." リンクをクリックしてください):

run addBook の実行結果

この図はインスタンスの関連図です。四角がそれぞれのインスタンスで、矢印がインスタンス間の関連を表します。四角で囲まれた整数も「整数のインスタンス」です。この図では "-8" から "7" までの整数のインスタンスが生成されています。

System のインスタンスは 2 個、 Book のインスタンスは合計 16 個生成されています (図には現れていませんが、 copies に含まれています) 。右端の Book は addBook の引数です。このインスタンスは両方の System から参照されており、両方の catalog と copies に含まれています。 copies に含まれる Book は 15 個ありますが、 catalog に含まれていません。 Author のインスタンスの 1 つ Author0 は、どの Book にも所属せずに独立していますが、著者名だけ登録することもあるでしょうから問題ないとします。

予想した結果と全然違う煩雑な内容だったのではないでしょうか？ addBook の定義は System に Book を追加するだけで、他の制約は一切ありません。 System のインスタンスは 1 つのみとも定義していませんし、異なるシステム間で同一の Book を共有してはいけないとも定義していません。在庫が 0 以上であるべきとも定義していませんし、 Author のインスタンスが必ず Book に所属しなければならないとも定義していません。

Alloy はあらゆる関係を考慮した多様なインスタンスを生成します。制約が少なければインスタンス間の関係も広がり、スコープが大きければ際限なく関係を網羅します。網羅したい関係が意図した範囲であればよいのですが、今回のモデルだと意図しない関係が多数含まれています。

そこで、ファクトを定義して不要な関係を取り除き、常に成立させたい制約を追加します。最初は System のインスタンスを 1 つに絞ります:

fact singletonSystem {
    #System = 1
}

System と Book のインスタンス間の関係が減り、少しすっきりしました。次に、在庫の数が必ず 0 以上になるファクトを追加します。 copies は System が管理するフィールドなので、 System のシグネチャにファクトを追加するのが簡単です (ファクトはシグネチャ側でも記述できます):

sig System {
    catalog: set Book,
    copies: catalog -> Int
} {
   all b: Book | copies[b] >= 0
}

在庫の数を 0 以上にする

在庫の数が負の数だったインスタンスが消えました。 copies の数も変わっていますが、 run で見つかる例はあくまで数あるうちの一つなので問題ありません。

このように、ファクトを定義すれば述語やアサーション以外でも制約をかけられます。ひとまずここでは在庫の数を 0 以上としましたが、システムによっては負の数も許容するかもしれませんし、在庫の数に上限があるかもしれません。これはインスタンスを確認するまで見落としていた仕様です。些細な仕様ですが、見落としを実装前に発見できてよかったと考えるか、それともこの程度の発見にかかるコスパが悪いと考えるか、それがモデル検査のトレードオフになると思います。

「本の在庫を追加する」を定義する

次は「本の在庫を追加する」述語を定義して検証します。この操作の内容と期待される結果を引用します:

• 「すでにシステムに登録されている本の在庫を1冊追加する」に期待されるのは「成功（すぐに在庫が1冊増える）」
• 「まだシステムに登録されていない本の在庫を1冊追加する」に期待されるのは「エラー」

今回も、成功とエラーを状態の変化で表します。「成功」は「在庫が1つ増える」、「エラー」は「在庫が増えない」とします:

pred addCopy [sys, sys": System, b: Book] {
    b in sys.catalog =>
        sys".copies = sys.copies + (b -> (sys.copies[b] + 1))
}

この中で見慣れない記述は (b -> (sys.copies[b] + 1)) でしょう (それぞれの括弧は省略可能です。ここでは式を区別しやすくするために括弧を明記しています) 。 -> は System.copies の型の定義と同じく関係を表します。キーと値みたいなものです。式中の -> も同じく、キーと値のペアを表します。

sys.copies[b] は sys.copies の値にキー b でアクセスします。 copies の値の型は Int なので、 sys.copies[b] は在庫数の取得を表します。したがって b -> (sys.copies[b] + 1) は、 b の在庫数を 1 増やしたペアになります。新しいペアを sys.copies に追加した結果が、状態変化後の sys".copies と等しいことを宣言しています。

左辺 b in sys.catalog は本が未登録であれば偽になりますが、前節で触れた通り => は含意演算子なので、左辺が偽であっても式全体は真になります。式全体が偽になるのは、左辺が真で右辺が偽の場合のみです。「本は登録済みだが在庫を追加できなかった」場合に偽になります。

アサーションを次のように定義します:

// すでに登録されている本の在庫を1冊追加する
assert addCopyExistingSuccess {
    all sys, sys": System, b: Book | 
        b in sys.catalog 
        implies addCopy[sys, sys", b] 
        implies sys".copies[b] = sys.copies[b] + 1
}

check addCopyExistingSuccess for 5

// まだ登録されていない本の在庫を1冊追加しようとする
assert addCopyNewFail {
    all sys, sys": System, b: Book | 
        b not in sys.catalog 
        implies addCopy[sys, sys", b]
        implies sys".copies[b] = sys.copies[b]
}

check addCopyNewFail for 5

最後の行は、 addCopy 実行後の在庫数を実行前の状態と比較します。「本が登録済みかつ在庫が 1 増えた」または「本が未登録かつ在庫に変化なし」であれば問題ありません。

反例を見つける

ここまでのアサーションはすべて成立する定義でした。今度はあえて反例を見つけてみましょう。積極的に反例を考えることで、予期しない挙動や設計上のエラーを特定できます。ユニットテストでも同じですね。

…なのですが、どうにも理解しやすい反例の書き方がわからず。反例が見つかったときの挙動を書いておくだけにします。

run や check の実行により反例が見つかると、ウィンドウ右に "Counterexample found. Assertion may be invalid." というメッセージがリンクつきで表示されます。クリックすると、反例のインスタンスを表示するウィンドウが開きます。以下は一例です:

見つかった反例のインスタンス

関数

検索操作の結果は、成功と失敗のどちらでも状態が変化しません。そのため、述語でどうにかするよりも関数とアサーションを組み合わせる方法が適しています。

ISBN で検索する関数を以下のように定義します:

fun findBookByIsbn [sys: System, i: Isbn]: set Book {
    {b: sys.catalog | b.isbn = i}
}

findBookByIsbn は、システムと ISBN を受け取って本の集合 (set Book) を返します。 | は or の意味ではなく、これまでに登場した | と同じです。 {...} は set を表します。リストの内包表記に近いです。

b: sys.catalog は sys.catalog に含まれるすべての要素 Book を変数 b とします。右辺の b.isbn = i により、 ISBN が一致すれば返します。

アサーションで検索の成功と失敗を確認します。コードは以下の通りです:

assert findBookByIsbnSuccess {
    all sys: System, i: Isbn, b: Book | 
        b in sys.catalog and b.isbn = i 
        implies b in findBookByIsbn[sys, i]
}

assert findBookByIsbnFail {
    all sys: System, i: Isbn, b: Book | 
        b not in sys.catalog and b.isbn = i 
        implies b not in findBookByIsbn[sys, i]
}

アサーションで使う式の内容はこれまでとほとんど同じです。述語を使っていた箇所が関数になっています。 findBookByIsbn は set Book を返すので、戻り値に対して b not in という記述ができます。

他の検索操作も同様に定義できます。詳細は記事の最後にあるコードを参照してください。

最終的なコード

残りの操作は、これまでに説明した内容で読めると思います。いかんせん初心者のコードなので、他にもっとよい書き方があるかもしれません。

sig Title {}

sig Author {}

sig Isbn {}

sig Book {
    title: Title,
    author: Author,
    isbn: Isbn,
}

sig System {
    catalog: set Book,
    copies: catalog -> Int
} {
   all b: Book | copies[b] >= 0
}

fact singletonSystem {
    #System = 1
}

// システムにまだ登録されていない本を追加する。成功の場合は状態変化（本の追加）がある。
pred addBook [sys: System, sys": System, b: Book] {
    b not in sys.catalog => sys".catalog = sys.catalog + b
}

// システムに登録されている本の在庫を1冊追加する。成功の場合は状態変化（在庫数の増加）がある。
pred addCopy [sys, sys": System, b: Book] {
    b in sys.catalog => sys".copies = sys.copies + (b -> (sys.copies[b] + 1))
}

// システムに登録されていて利用可能な在庫がある本を貸出する。成功の場合は状態変化（在庫数の減少）がある。
pred borrowCopy [sys: System, sys": System, b: Book] {
    (b in sys.catalog and sys.copies[b] > 0) => sys".copies = sys.copies + (b -> (sys.copies[b] - 1))
}

// システムに登録されている本を返却する。成功の場合は状態変化（在庫数の増加）がある。
pred returnCopy [sys, sys": System, b: Book] {
    b in sys.catalog => sys".copies = sys.copies + (b -> (sys.copies[b] + 1))
}

// ISBNで本を検索し、結果を返す関数
fun findBookByIsbn [sys: System, i: Isbn]: set Book {
    {b: sys.catalog | b.isbn = i}
}

// タイトルで本を検索し、結果を返す関数
fun findBookByTitle [sys: System, t: Title]: set Book {
    {b: sys.catalog | b.title = t}
}

// 著者名で本を検索し、結果を返す関数
fun findBookByAuthor [sys: System, a: Author]: set Book {
    {b: sys.catalog | b.author = a}
}

assert addNewBookSuccess {
    all sys, sys": System, b: Book |
        b not in sys.catalog
        implies addBook[sys, sys", b]
        implies b in sys".catalog
}

check addNewBookSuccess for 5

assert addExistingBookFail {
    all sys, sys": System, b: Book |
        b in sys.catalog
        implies addBook[sys, sys", b]
        implies b in sys".catalog
}

check addExistingBookFail for 5

assert addCopyExistingSuccess {
    all sys, sys": System, b: Book | 
        b in sys.catalog 
        implies addCopy[sys, sys", b] 
        implies sys".copies[b] = sys.copies[b] + 1
}

check addCopyExistingSuccess for 5

assert addCopyNewFail {
    all sys, sys": System, b: Book | 
        b not in sys.catalog 
        implies addCopy[sys, sys", b]
        implies sys".copies[b] = sys.copies[b]
}

check addCopyNewFail for 5

assert borrowCopySuccess {
    all sys, sys": System, b: Book | 
        b in sys.catalog and sys.copies[b] > 0 
        implies borrowCopy[sys, sys", b] 
        implies sys".copies[b] = sys.copies[b] - 1
}

check borrowCopySuccess for 5

assert borrowCopyNoStockFail {
    all sys, sys": System, b: Book | 
        b in sys.catalog and sys.copies[b] = 0 
        implies not borrowCopy[sys, sys", b]
}

check borrowCopyNoStockFail for 5

assert borrowCopyNotRegisteredFail {
    all sys, sys": System, b: Book | 
        b not in sys.catalog 
        implies not borrowCopy[sys, sys", b]
}

check borrowCopyNotRegisteredFail for 5

assert findBookByIsbnSuccess {
    all sys: System, i: Isbn, b: Book | 
        b in sys.catalog and b.isbn = i 
        implies b in findBookByIsbn[sys, i]
}

assert findBookByIsbnFail {
    all sys: System, i: Isbn, b: Book | 
        b not in sys.catalog and b.isbn = i 
        implies b not in findBookByIsbn[sys, i]
}

check findBookByIsbnSuccess for 5

check findBookByIsbnFail for 5

assert findBookByTitleSuccess {
    all sys: System, t: Title, b: Book | 
        b in sys.catalog and b.title = t 
        implies b in findBookByTitle[sys, t]
}

assert findBookByTitleFail {
    all sys: System, t: Title, b: Book | 
        b not in sys.catalog and b.title = t 
        implies b not in findBookByTitle[sys, t]
}

check findBookByTitleSuccess for 5

check findBookByTitleFail for 5

assert findBookByAuthorSuccess {
    all sys: System, a: Author, b: Book | 
        b in sys.catalog and b.author = a 
        implies b in findBookByAuthor[sys, a]
}

assert findBookByAuthorFail {
    all sys: System, a: Author, b: Book | 
        b not in sys.catalog and b.author = a 
        implies b not in findBookByAuthor[sys, a]
}

check findBookByAuthorSuccess for 5

check findBookByAuthorFail for 5

まとめ

数学的な基盤を持つ言語で仕様を記述し、設計や振る舞いを検証する方法を形式手法と言います。はじめからこの単語を出してしまうと敬遠される可能性が高いため、本記事では触れませんでした。私も単語は知っていましたが、自分とは縁がないものと思っていました。

形式手法は、仕様や実装のミスが致命的な問題を引き起こす、組み込み系や人命に関わるシステムなどの分野で活用されています。仕様記述言語は Alloy の他にも多く開発されており、使われるツールはプロジェクトによって異なります。

冒頭でも触れたように、個人的に仕様を考えたり確認するのにモデル検査を気軽に使えないかなあと思っています。一般的なアプリや Web サービスでも有用だと思いますが、学習コストが高いですし、 Alloy は実装用のコードを出力するわけではないので、チーム開発に組み込むのはあまり現実的でないかもしれません。

仕様記述言語の中でも Alloy は比較的学習コストが低いほうだと思います。いまは AI にいくらでも質問できますから、試してみるのも一興ではないでしょうか？ (ただ、 ChatGPT や GitHub Copilot が出力するコードの質はいまいちだと思います)

よかったらバッジをいただけると嬉しいです。コーヒー代の足しにします。

参考資料

書籍

• 抽象によるソフトウェア設計 ―Alloyではじめる形式手法: Exercises の Address Book がサンプルコードとして解説されています。専門的な知識がなくても思ったより読みやすいです。

Web

• Alloy Tutorial: ファイルシステムを例として取り上げています。
• Formal Software Design with Alloy 6
• Alloy Docs: 公式っぽいタイトルに見えますが非公式です。