ツールを頼ってペアワイズ法で組み合わせテストを生成してみたら、出現しない組み合わせがあったので不安になり、でもその確認にも自分の頭を使わずにAlloy Analyzerにやらせようと、しかも楽してそのソースを自動生成しようとやってみたら、Alloy超入門の事例として悪くない気がしてきたので、4,500字くらいでそれをいい加減に紹介する投稿

本稿ではPICT-PAPPが生成するAlloyソースの解説をします。
生成されるソースは「ペアワイズツールが生成しなかった組み合わせが間接禁則である（ペアが生成されなくて良い）ことを検証する」ものです。
(PICT-PAPPが何であるかということについては、別稿に記載しましたのでそちらを見てください。）

「やさしい事例から学ぶAlloy超入門」になっていると思います。同時に、すぐに実務にも役立てることができると思います。これを出発点として、少しずつ必要な書き換えを、それに必要なことだけを学びながら実施していけば、業務の中で活用しながら継続的に理解を深めていけるのではないか、と思っています。

下記の説明を読み進めていくとわかると思いますが、ここで説明するAlloyのソースはペアワイズ法の組み合わせテストを生成するツール(CIT-BACHあるいはPICT)に与えるために記述するソースによく似ています。

ですので、「よし、ここでペアワイズ法やHAYST法と併せて、ついでにAlloyも理解して明日から使おう！」といった動機で読んでいただけると良いかと思います。
（Alloyを既にご存知の方はこの記事を読む価値はありません。
生成されるソースを見れば、何をしたいのか、どう実現しているのか、一目瞭然だと思いますので、それだけで済むと思います。）

Alloyのアプローチの特徴は、次のようなことだと思います。
まず、仕様記述については形式手法に倣ったものになっています。
しかし、その解析方法は従来のそれとは異なり、完全に自動化され即座にフィードバックが得られるようなものに置き換えられています。
従来からよくある定理証明に基づく方法を採らず、有限のケースからなる空間しか探索しないことにするのです。
それゆえ「完全」ではないということになってしまうのですが、その代わりに証明の手間もかかりませんし、テストケースを用意する必要もなくなります。
いや、「テストケースは1つだけ必要である」と言った方が正確かもしれません。
テストケースを1つ書く程度の簡潔さで十分ですが、検査すべき性質を書く必要はあるからです。やることはそれだけです。
先に「有限のケースからなる空間しか」という表現をしましたが、探索可能な空間は巨大(10億通り以上)なので、テストでは達成不可能な高いカバレッジを実現することができます。
(実は形式手法を採用している現場でも、ちゃんと証明までしているケースは限られているようです。手間がかかるのでやってられないということでしょう。それでも良いのです。ちゃんと仕様記述しただけで大分効果が上がるので、それで満足できることが多いということなのでしょう。そういう現実があるということを踏まえると、「完全」ではないという負の側面よりも、自動化され即座にフィードバックが得られる解析機能が付いている、という側面の方を大いに評価すべきと思います。）

さて、前置きが長くなってしまっているので、早速ソースの説明に入りましょう。
まずは全体的な意味や各部の役割が掴めることが重要と思いますので、思いっきり大まかな説明をします。また、用語についても厳密に使い分けることよりも、取り急ぎそう思っておけば理解が早い方を優先して使います。もう少し厳密な説明はまた別の機会にしますので、そう了解してください。

説明のために取り上げる具体例ですが、複合機の事例とします。PCから印刷するときの機能指示部分で、画面としては以下のような表示が出ます。

ここでは上図で赤く示した3箇所の設定項目(次の図の総当たり表では因子・水準として示されている)の部分に注目するものとします。
（これは、PICT-PAPPによるPairwise組み合わせテストを設計する手順を説明する記事の中で禁則の取り扱いを示しましたが、その禁則部分だけを抽出した例となっています。）

どんな禁則が定義されているかといえば、印刷する原稿の向きと両面印刷するかどうかということで、とじしろの位置を制限するということで、次の表の通り×が付いていてピンク色になっているセルの組み合わせが禁止されている、という事例です。

それでは、この事例に対して生成されるソースの説明に入ります。

enum 原稿の向き {たて, よこ}
enum 両面 {しない, 短辺とじ, 長辺とじ}
enum とじしろ {なし, 短辺上, 短辺左, 短辺右, 短辺下, 長辺上, 長辺左, 長辺右, 長辺下}

この部分はCIT-BACHやPICTのソースに似ていますね。因子・水準を定義しています。
enumは列挙型のデータを定義するもので、様々なプログラミング言語で見慣れていることと思います。
各因子について、取り得る水準の全てを要素として持つ集合として、それに因子名を付けて定義しています。

sig システム {
    原稿の向きの水準:one 原稿の向き,
    両面の水準:one 両面,
    とじしろの水準:one とじしろ
}

続いて、テスト対象のシステム（先の因子・水準を抽出した元のシステム)を定義しています。
sigは構造体あるいはオブジェクトのクラスを定義するものだと思っておいて構いません。
ここでは、システムは先に定義した全ての因子を要素として持つ集合として定義しています。
ただし、先に定義した因子名は取り得る水準全ての集合でした。システムの各因子には集合が入るわけではなく、その中の要素のどれか一つになるはずです。ですから、因子名そのものは使わず、因子名に「の水準」という文字列を連結した名前を使っています。
そして、":one 因子名"で、因子名の集合のいずれか必ず一つの要素が入るものとしています。

つまり、それぞれの因子が先に定義した水準の集合のいずれかの要素になっているはずのシステムである、という最低限の性質を示しただけの定義になっているわけです。

{
    原稿の向きの水準=たて and 両面の水準=しない=>とじしろの水準!=短辺左
    原稿の向きの水準=たて and 両面の水準=しない=>とじしろの水準!=短辺右
    原稿の向きの水準=たて and 両面の水準=しない=>とじしろの水準!=長辺上
    原稿の向きの水準=たて and 両面の水準=しない=>とじしろの水準!=長辺下
    原稿の向きの水準=たて and 両面の水準=短辺とじ=>とじしろの水準!=短辺左
    原稿の向きの水準=たて and 両面の水準=短辺とじ=>とじしろの水準!=短辺右
    原稿の向きの水準=たて and 両面の水準=短辺とじ=>とじしろの水準!=長辺上
    原稿の向きの水準=たて and 両面の水準=短辺とじ=>とじしろの水準!=長辺左
    原稿の向きの水準=たて and 両面の水準=短辺とじ=>とじしろの水準!=長辺右
    原稿の向きの水準=たて and 両面の水準=短辺とじ=>とじしろの水準!=長辺下
    原稿の向きの水準=たて and 両面の水準=長辺とじ=>とじしろの水準!=短辺上
    原稿の向きの水準=たて and 両面の水準=長辺とじ=>とじしろの水準!=短辺左
    原稿の向きの水準=たて and 両面の水準=長辺とじ=>とじしろの水準!=短辺右
    原稿の向きの水準=たて and 両面の水準=長辺とじ=>とじしろの水準!=短辺下
    原稿の向きの水準=たて and 両面の水準=長辺とじ=>とじしろの水準!=長辺上
    原稿の向きの水準=たて and 両面の水準=長辺とじ=>とじしろの水準!=長辺下
    原稿の向きの水準=よこ and 両面の水準=しない=>とじしろの水準!=短辺上
    原稿の向きの水準=よこ and 両面の水準=しない=>とじしろの水準!=短辺下
    原稿の向きの水準=よこ and 両面の水準=しない=>とじしろの水準!=長辺左
    原稿の向きの水準=よこ and 両面の水準=しない=>とじしろの水準!=長辺右
    原稿の向きの水準=よこ and 両面の水準=短辺とじ=>とじしろの水準!=短辺上
    原稿の向きの水準=よこ and 両面の水準=短辺とじ=>とじしろの水準!=短辺下
    原稿の向きの水準=よこ and 両面の水準=短辺とじ=>とじしろの水準!=長辺上
    原稿の向きの水準=よこ and 両面の水準=短辺とじ=>とじしろの水準!=長辺左
    原稿の向きの水準=よこ and 両面の水準=短辺とじ=>とじしろの水準!=長辺右
    原稿の向きの水準=よこ and 両面の水準=短辺とじ=>とじしろの水準!=長辺下
    原稿の向きの水準=よこ and 両面の水準=長辺とじ=>とじしろの水準!=短辺上
    原稿の向きの水準=よこ and 両面の水準=長辺とじ=>とじしろの水準!=短辺左
    原稿の向きの水準=よこ and 両面の水準=長辺とじ=>とじしろの水準!=短辺右
    原稿の向きの水準=よこ and 両面の水準=長辺とじ=>とじしろの水準!=短辺下
    原稿の向きの水準=よこ and 両面の水準=長辺とじ=>とじしろの水準!=長辺左
    原稿の向きの水準=よこ and 両面の水準=長辺とじ=>とじしろの水準!=長辺右

}

この部分は再びPICTやCIT-BACHのソースに似ていますね。それらのソースにおいては制約定義部分です。
こちらのソースではここ（{}内）はファクトを定義する部分です。
ファクトは常に成り立つ制約である、と理解しておけば良いです。（ここで「常に成り立つ」はこのシステムとしてとして変わることなく常に成り立つという意味です。例えばPICTの説明などでは「常に成り立つ」を「条件部無しに」の意味で用いることが多いので、その違いに注意してください。）
通常、ファクトには'{'の手前で名前が付けられます。(名前は無くても構いません。)
しかし、ここでのファクトはsigの直後に置かれています。この場合、そのファクトは直前のsigに関するファクトであると解釈されます。つまりここではシステムに関するファクトということになります。ですから、CIT-BACHやPICTのソースに記載した制約と全く同じ制約を持っているはずであり、似ているのも当然、というか表記方法が若干異なるだけで、その内容は全く同じです。

pred 組合せ状態が存在する(s:システム) {
    s.とじしろの水準 = 短辺左 && s.原稿の向きの水準 = たて ||
    s.とじしろの水準 = 短辺右 && s.原稿の向きの水準 = たて ||
    s.とじしろの水準 = 長辺上 && s.原稿の向きの水準 = たて ||
    s.とじしろの水準 = 長辺下 && s.原稿の向きの水準 = たて ||
    s.とじしろの水準 = 短辺上 && s.原稿の向きの水準 = よこ ||
    s.とじしろの水準 = 短辺下 && s.原稿の向きの水準 = よこ ||
    s.とじしろの水準 = 長辺左 && s.原稿の向きの水準 = よこ ||
    s.とじしろの水準 = 長辺右 && s.原稿の向きの水準 = よこ ||
    s.とじしろの水準 = 長辺上 && s.両面の水準 = 短辺とじ ||
    s.とじしろの水準 = 長辺左 && s.両面の水準 = 短辺とじ ||
    s.とじしろの水準 = 長辺右 && s.両面の水準 = 短辺とじ ||
    s.とじしろの水準 = 長辺下 && s.両面の水準 = 短辺とじ ||
    s.とじしろの水準 = 短辺上 && s.両面の水準 = 長辺とじ ||
    s.とじしろの水準 = 短辺左 && s.両面の水準 = 長辺とじ ||
    s.とじしろの水準 = 短辺右 && s.両面の水準 = 長辺とじ ||
    s.とじしろの水準 = 短辺下 && s.両面の水準 = 長辺とじ
}

この部分は確認したいことを記述しています。(1階述語論理の)述語形式で記述します。
predが述語を定義することを表しています。
'組合せ状態が存在する'が述語名です。sは変数名です。つまり、変数が一つの次の述語が定義されていることになります。

組合せ状態が存在する(s)

sの右に記述されている ':システム' ですが、これはsの型がシステムである、あるいはsには集合であるシステムの要素が入ると示されていると解釈すれば良いです。
その後の{}内にはこの述語が満たすべき制約を記載します。

まず、's.とじしろの水準' のような '.' の入った表現ですが、これも様々なプログラミング言語で見慣れた使い方になっていると思います。sを構造体と考えればその属性、クラスだと思うならばそのスロットの値を指すものだと解釈すれば良いです。

この具体例では何が記載されているかというと、PICT-PAPPの総当たり表で黄色に塗りつぶされた、いずれかの値の組み合わせを有することを表しています。
つまり、総当たり表で禁則だと指定はしなかったのに、CIT-BACHやPICTが生成しなかった2因子間組み合わせが、本当に生成されなくて良いのか、を確認しようというわけです。
このように、直接には禁則だとこちらが示していないのに、他に示した制約条件から結果的に必ず禁則になるものをHAYST法では間接禁則と呼んでいます。
つまり、ここの述語定義の具体例の場合、この黄色い部分の組み合わせは本当に間接禁則なのか？と確認する述語を定義したことになります。

run 組合せ状態が存在する for 1 but exactly 1 システム

最後、この部分は、解析器に何をどのように解析して欲しいかを指示しています。

この具体例の場合、述語 '組合せ状態が存在する' が成立するような システム (そのようなインスタンス)があるかを調べさせています。

この具体例の場合、ツールに頼らなくても、ちょっと考えれば黄色く示された組み合わせはいずれも間違いなく間接禁則になっていることが確認できると思います。

Alloyによる解析結果も同じで、そんな禁則組み合わせをたった一つでも持つようなシステムの状態は一つも見つけられなかったということで、No instance found.を返してきます。

これでめでたく出現していない組み合わせはどうやら間接禁則であると確認できました。

では、今度はちょっと、述語の制約を変更して、禁則ではないものを含めてみて、それをちゃんと見つけられるか実験してみましょう。

述語の制約の最後の行にORの演算子を加え、さらにもう一行、今度はあきらかに禁則ではない組み合わせを加えてみます。

    s.とじしろの水準 = 短辺下 && s.両面の水準 = 長辺とじ ||
    s.とじしろの水準 = なし && s.両面の水準 = 長辺とじ

これで解析を指示すると、添付の図の通り、ちゃんとその組み合わせを採るインスタンスが発見されることになります。

右側のInstanceは青い文字で示されていますが、これはリンクになっているのでクリックすると以下のウインドウが表示され、具体的にどんなインスタンスなのかを知ることができます。（表示の形式は何通りかあり、選べます。）

他にインスタンスはないのか知りたいときは、Nextボタンを押します。

もう1回、Nextボタンを押すと

もうこれ以上は他のインスタンスが見つからないということです。

ということで、今回の説明は以上になります。

「なーんだ、Alloyってとっても簡単！便利！」
「早速明日から使ってみよう」

という人が増えると良いな、と思います。

日本語訳された良書『抽象によるソフトウェア設計−Alloyではじめる形式手法−』もあり、学びやすいです。

今回の説明は、ここまでとなります。

通常、何かの説明をはじめるときには、まずその意義(何のためにそれを理解する必要があるのかという話)から始めるのが良いと考えており、いつもはそうしてきているつもりなのですが、今回はちょっと事情があって、「本当は何のため」なのかの説明を飛ばしています。(いずれ別稿で示したいと思っています。)