はじめに（前置き）
こんにちは、世界。
ログラスでQAエンジニアを担当している大平です。
突然ですが、みなさん、仕様のレビューをしていますか？レビューをしている場合は、どうやって行っていますか？
私はQAエンジニアとして、過去に実施したテスト経験や起きた不具合、既存の機能との整合性や矛盾点、競合製品がどうなっているか、テストのしやすさなどの観点でレビューを実施します。
（ちなみにレビューについては、書籍「間違いだらけの設計レビュー」がお勧めです）
ただ、過去を振り返ると、私の技量が足りないため、仕様の詳細な部分の指摘が漏れ、後工程で発覚することがQAエンジニアのキャリアの中で何度もありました。もちろん、複雑な仕様については、デシジョンテーブルや状態遷移図で整理しているのですが、それでも漏れてしまうことがあり、何か良い方法はないか、どうアプローチすべきかを約10年間悩んでいました。
そんなモヤモヤを抱えて10年ほど過ごしていたのですが、あるイベントに参加した際に「QAエンジニアなのに形式手法を知らないのですか？」（意訳）と驚かれたことがありました。その時、恥ずかしながら、私は形式手法について全く知識がありませんでした。
調べてみると、弊社でアジャイルコーチをしている @bonotake さんが、形式手法に関する書籍『抽象によるソフトウェア設計－Alloyではじめる形式手法－』を翻訳していることを知りました。（偶然）
@bonotake さんにお話を伺うと、「複雑な仕様には形式手法が使えると思いますよ」と教えていただき、興味が湧いたので、Alloy を学んでみることにしました。
Alloyは、形式手法を簡潔に適用できるツールのひとつです。Alloyでは、システムの仕様を形式的に記述し、モデル検査のエンジンを通じてその仕様が正しいか、矛盾がないかを確認することができます。
しかし、Alloyを使いこなすには、形式手法の基礎知識とAlloy独自の記述方式の理解が必要で、（私には）なかなかハードルが高い印象でした。そのため、Alloyを「学ぶこと」にフォーカスしすぎて、本来の目的である仕様検証まで、なかなか到達できないという新たな問題が発生したのでした。
（書籍『抽象によるソフトウェア設計－Alloyではじめる形式手法－』はとても良書です。素人の私でもわかりやすく書いてありますが、それでもAlloyで自分が意図した記述をするには、ハードルが高かったです。）
なかば諦めかけていたのですが、再び @bonotake さんから、「AIがあれば、あまり難しく考えることなく使えるはずだよ」（意訳）というアドバイスをもらい、再チャレンジすることにしました！
そういうわけで、この記事は、CursorのAIチャット機能を活用して、なるべくハードル低く、Alloyにチャレンジする記録です。
そもそもAlloyで何をしたいのか
Alloyは、形式的に記述したシステム全体のルールや制約を解釈し、例を自動生成してくれます。その自動生成された例を人間が目で見て確認することによって、矛盾がないかを判断することができます。
Alloyのツールを使って、記述されたシステムが満たすべきルールや制約をもとに可能な状態空間を探索し、矛盾や不整合がないかを確認する方法です。
この効果は、実例マッピングの効果と同じです。
（実例マッピング知りたい方は、こちらの記事がおすすめです）
実例マッピングには、1からルールを作るケースと既存のルールを改善するケースがあります。
既存のルールを改善するケースでは「既存のルールに対して実際にある具体例を挙げ、その例がルールで説明しきれるか、きちんと当てはまっているかを議論し、新たな知見を得る」という方法で、Alloyと基本的に同じアプローチになります。
実例マッピングで既存ルールを改善する場合との違いは、実例マッピングでは関係者で実際の具体例を出していくことに対して、Alloyではルールを解釈し自動生成された例を使うという点です。
Alloyでは、解釈し自動生成された例を確認することで、矛盾点や足りない部分に気づくことができます。これを利用すれば、気づかなかったルールを発見したり、詳細化することができます。
流れとしては、以下のアプローチになります。
Step1.ルールを記述する
Step2.モデルを確認
Step3.矛盾や抜けがある場合はルールを追加する
（納得できるまで、2と3を繰り返す）
Step1とStep3では、Alloyの知識が必要になりますが、この部分にCursorのAIチャット機能を活用します。AIと会話しながら、Alloyの記述に落とし込んでモデルを確認し、仕様を詳細化していくというアプローチになります。
ちなみに、まったくAlloyを知らないと難しい部分があるので、私は以下の主な要素ぐらいは覚えました。（参考までに）
- Signature（シグネチャ）：システム内の構成要素やデータ構造を定義（オブジェクト指向のクラスやER図のエンティティに相当する）
- Fact（ファクト）：システム全体が常に保つ制約を記述
- Predicate（記述）：システムが特定の状況下で満たす条件や状態、状態の変化などを記述
Cursorと一緒にAlloyのチャレンジ
※事前準備でCursorをインストールし、拡張機能でAlloyを追加している前提です。Cursorの使い方については、省略します。
今回は、あるシステムのユーザ管理の仕様を作成にチャレンジしてみます。
まず、初めにCursorで、AIチャット機能を起動して、以下の入力をしてみます。
あるシステムのユーザ管理の仕様の作成をお願いします。
- あるシステムのユーザ管理機能ではユーザーを登録できます。
- ユーザーは一意のIDを持ちます。
- ユーザーは一つのロール持ちます。
-ロールは、一般と管理者があります。
以下の記述が生成されました。
// ユーザーを表すシグネチャ
sig User {
id: one Int, // 一意のID
role: one Role // ユーザーが持つロール
}
// ロールを表す列挙型
abstract sig Role {}
one sig Normal, Admin extends Role {} // 一般ユーザーと管理者
// ユーザーIDは一意であることを保証する制約
fact UniqueUserIds {
no disj u1, u2: User | u1.id = u2.id
}
// システムの状態を確認するためのアサーション
assert UserHasOneRole {
all u: User | one u.role
}
// サンプルの実行のためのpred
pred show {
#User > 1 // 複数のユーザーが存在する状態を表示
}
run example {
}
以下のモデルが生成されます。（一部）
モデル1
モデル2
モデルを確認すると、管理者権限（admin）のユーザーが存在しない場合があることがわかりました。
そのため、管理者権限（admin）のユーザーが必ず1つ以上存在するという仕様を追加します。
以下の仕様を追加してください。
-システムのユーザ管理では、 管理者権限をもつユーザが1つ以上存在する必要がある
記述が以下のように修正されました。
module system/IDM
// ユーザーを表すシグネチャ
sig User {
id: one Int, // 一意のID
role: one Role // ユーザーが持つロール
}
// ロールを表す列挙型
abstract sig Role {}
one sig Normal, Admin extends Role {} // 一般ユーザーと管理者
// ユーザーIDは一意であることを保証する制約
fact UniqueUserIds {
no disj u1, u2: User | u1.id = u2.id
}
// システムの状態を確認するためのアサーション
assert UserHasOneRole {
all u: User | one u.role
}
+ // 少なくとも1人の管理者が存在することを保証する制約
+ fact AtLeastOneAdmin {
+ some u: User | u.role = Admin
+ }
// サンプルの実行のためのpred
pred show {
#User > 1 // 複数のユーザーが存在する状態を表示
}
run example {
}
以下のモデルが生成されます。（一部）
モデル1
モデル2
これで、管理者権限（admin）のユーザーが必ず1つ以上存在するようになりました。
今回は簡単な仕様でしたが、モデルを確認することで見逃しがちな仕様を明文化することができました。Alloyで生成された例を確認することで、このような暗黙的な仕様や記載自体を忘れがちなルール、またミスや漏れを防ぐ助けとなることを実感できました。
まとめ
Alloyは非常に強力なツールですが、初心者にとっては、使いこなすまでの敷居は低くありません。
今回のチャレンジを通して、CursorのAIチャット機能を使うことで、形式手法をより手軽に活用できるようになり、システムの設計をより高い品質で進められる手応えを感じました。
まだ実践するには知識や工夫が必要ですが、AIを駆使しながら、プロダクト開発の本質的な課題にアプローチしていきたいと思います。（つづく）
株式会社ログラスは「良い景気を作ろう。」をミッションに、企業経営を推進する次世代型経営管理クラウド「Loglass 経営管理」を開発し提供しています。
Discussion