導入：考えない名探偵

我々には、問題をみると「どうやったら解決できるか」と考える癖がついている。
数独のようなパズルを見ても、どう考えたら解にたどり着けるか自分なりのアルゴリズムを探っている。

しかしここにコンピュータがある。
コンピュータが人間に勝る大きな点は圧倒的な計算速度による力技であり、総当たりの威力である。
総当たりの威力をもってすれば、数独のような単純な問題は考えるまでもないのだ。

状況を聞いただけで、考えるそぶりも見せずに解を出すそれは、さながら名探偵のよう。
考えない名探偵を相棒に得たとき、我々は何をできるのだろうか。

形式手法のひとつである Alloy、ツール Alloy Analyzer はこの名探偵のような存在です。
これを使う人間に必要なことは的確に状況を伝えること、すなわち 正確に仕様を記述すること です。
問題の解法をプログラミングするのではなく、ルールや状況を記述するだけで、過程や結果を見せてくれる。
そうやってパズルを解かせるのは、自分で解くのともプログラミングで解かせるのとも違った面白さがあります。
そしてもちろん、正確な仕様記述は人間がプログラミングする場合にも役立ちます。

対象読者

パズルを解かせてみたい人、形式手法って聞いたことある(ない)けど難しそうという人など。

環境

Visual Studio Code に Alloy プラグインがあるので、それを使うのがお勧めです。
シンタックスハイライト、VS Code内からの実行、マークダウン内埋め込みからの実行などとても便利です。

Alloyの勉強には、やはり書籍『抽象によるソフトウェア設計 ―Alloyではじめる形式手法』が必要でしょう。
例題としてパズルも数多く載っていて楽しめます。
いきなり通読するのは難しいかと思いますので、読めそうなところを読んで、あとは必要に応じて参照するとよいでしょう。
いきなり書籍を買いたくない場合は、リストを見て雰囲気を感じるところからでいいでしょう。

パズル(1) ウソつき問題

問題

よくある、誰がウソつきかを当てる問題。
レイトン教授の例が Alloy 紹介の SlideShare に上がっていたので、やってみよう。

リストと結果

両含意<=> を使うと簡潔に書ける。
問題文を書き写しただけで解き方を一切書いていないことに注目。
Qiita では Alloy のシンタックスハイライトが効かないのが残念（Scalaが一番近い気がする）

puzzle1.als

/* レイトン教授 より
    https://www.slideshare.net/osiire/alloy-analyzer
*/

// 本当のことしか言わないトンホー種とウソしか言わないソーウ種
enum 牛種 {トンホー種, ソーウ種}
abstract sig 牛 {type:牛種}
one sig A,B,C,D,E extends 牛 {}     // ５頭の牛がいる

fact {
    #(type.トンホー種) = 2    // ２頭はトンホー種（他はソーウ種）
    // 「X <=> Y」は、(XならばY) かつ (YならばX)
    (A.type = トンホー種) <=> (D.type = ソーウ種)       // A「Dはソーウ種だね」
    (B.type = トンホー種) <=> (C.type != トンホー種)    // B「Cはトンホー種じゃないよ」
    (C.type = トンホー種) <=> (A.type != ソーウ種)      // C「Aはソーウ種じゃない」
    (D.type = トンホー種) <=> (E.type = ソーウ種)       // D「Eはソーウ種です」
    (E.type = トンホー種) <=> (B.type != トンホー種)    // E「Bはトンホー種じゃないぞ」
}

run {}

// 以降は答え合わせ
// 「Bはトンホー種である」に対する反例があるか確認する
check { B.type = トンホー種 }

// 「Dはトンホー種である」に対する反例があるか確認する
check { D.type = トンホー種 }

解説：両含意

日常言語の感覚とは異なるが、論理学の立場では「宿題やったらおやつ食べていいよ」は宿題をやらなかった場合に言及していないことになる。
宿題をやらなくてもおやつを食べていいかもしれないのだ。
形式仕様記述として明確さを求めるため、上記の言葉は Alloy では宿題やった => おやつ食べていいと書き、「おやつ食べていいのは宿題やったとき」を含む宿題やった <=> おやつ食べていいと明確に書き分ける。

日常言語でも「食べたらなくなる」の例なら「なくなるのは食べたとき」と言っているわけではない。
「たら」「なら」の意味が単独では確定しないということで、自然言語解析分野の話になる。

※ていうか、プログラマー的には
　　if (宿題やった) おやつ食べていい
　　if (食べた) なくなる
　と書いたらそういう意味になるのは当たり前だよね
　逆も必要ならそう書かないとダメで、よく使う表現だから簡単に書き分けられるよというだけの話

参考

SlideShare : レイトン教授で始めるAlloy Analyzer入門
Daniel Jackson : 抽象によるソフトウェア設計 ―Alloyではじめる形式手法
本家サイト : alloy
(モデル置き場) : jpwgad/alloy-models

あとがき

Alloyを勉強して２ヶ月強、それなりに使えるようになってきました。
ネットに残っている記事は古かったり掲載リストが難しかったりしたので、今やるならこうというサンプルを放流してみようかと。
形式手法を楽しいと感じて、気軽に付き合っていく助けになれたらいいなと思います。