Alloy で形式手法を始めてみた！～導入編～
Alloy とは
Alloy は構造の記述とその探索のためのツール．例えば，セキュリティホールの発見や，定義されたネットワークトポロジーの中で起こりうる構造の列挙するなど，定義を書いてその例を列挙したり，ある性質が成り立つかどうかを反例を探すことで確かめたりできるツールです．
例えば，システム開発で「これこれこんな感じで作ってくれ～」と言われて作ったがバグが見つかった，という経験はないでしょうか？この手の記事を読む方なら，きっとあるでしょう．
作る前に仕様の矛盾に気づけないだろうか？という疑問に対する答えの一つが，形式手法です．
"数学を基盤として仕様を記述したり，ある種の性質を検証したりする技術"を形式手法といいます．
Alloy は，記述された仕様と証明したい性質を SAT に還元して SAT ソルバで問いてしまおうというものです．これにより，完全ではないが小さいスコープの範囲で自動で例を列挙できるようにし，利便性を高めたツールなのです．
…というとなんだか難しく聞こえますが，要は「作りたいものの構造を記述できる」かつ「作りたいものがある性質（バグの有無など）を検証できる」ツールです．
論理学のような数学的なバックグラウンドがあるに越したことはないですが，なくても使えます．
Alloy を導入してみよう
Alloy を使うには，Alloy の公式サイトから Alloy Analyzer の jar を落として利用するか，VSCode の拡張を利用するかの 2 パターンがあります．
個人的には言語ごとに個別の専用のエディタを使いたくないため，VSCode で書いています．ここでは，VSCode でのインストール手順を紹介します．
前提条件
- VSCode がインストールされていること
- Java がインストールされていること
どちらもググれば出ますので，各自お願いいたします．
私は，Java は OpenJDK 11 を利用しています．
インストール手順
Alloy の拡張機能のインストール
拡張機能の検索窓に "Alloy" と入力し，インストールします．
インストール作業はこれだけ！
動作確認
インストール後，Ctrl + N
// 投げる人
one sig Player {
, first: TryFirst
, second: TrySecond
, third: TryThird
}
// 投球の抽象シグネチャ
abstract sig Try{}
// 第 10 フレームの 1 投目から 3 投目
one sig TryFirst, TrySecond, TryThird extends Try {
, result: TryResult
}
// 各投球の結果
enum TryResult {
Ordinal // 0 - 9 本であり，かつスペアでない
, Spare // スペア
, Strike // ストライク
, NotTried // 投球せず
}
Ctrl + S
保存後，シンタックスハイライトが機能します．また，"Execute" が表示されますので，クリックしてみます．
画面右側に実行結果が表示されますので，リンクをクリックしてみると，モデルが表示されます．
この結果は，Player によるボウリングの第 10 フレームでの投球結果の一つを表しています．
TryFirst が 1 投目，TrySecond が 2 投目，TryThird が 3 投目です．
コピペで書いた仕様が正しくないため，どの結果も NotTried，つまり 1 球も投球していないパターンが表示されています．
この第 10 フレームの仕様を検証し，修正まで行った記事がありますので，興味があれば御覧ください．
なるべく開発現場での実践的な使い方になるように書いたつもりです！
Alloy の他に，TLA+ を使った記述も行っています．
参考：【形式手法】ボウリング第 10 フレームを Alloy と TLA+ (PlusCal) で定式化
まとめ
- VSCode で Alloy をサクッと始められる
- シンタクスハイライトが利用できる
- ボタン一つで実行できる
VSCode の拡張はやっぱ便利だな～．
次回以降，Alloy の使い方について解説していこうと思います．
一応，チートシートの記事は書いていますが，自分の復習やチートシートのブラッシュアップも兼ねてゴリゴリ説明していければと思います．
では！
コメント