#formal.methods

図式を使えばいいのに 図式は非常に便利であるが、その表現力には制限がある。筆者はモデルの構造をスケッチするのに図式を使い、それをAlloyのテキストに起こしている。図による入力は実際にはあまり便利とはいえない。ツールでは図式を描くよりもテキストを入力するほうが少ない労力で済む。一方、図を使った出力は欠かすことができない。

ソフトウェアのモデルを自動解析機で探索する経験は、心躍ると同時に痛みを伴うものである。たいていの設計者は、仲間からのレビューによる恩恵を受けている。それは誤りや抜けを見つける確実な方法である。しかしながら、自分の書いたモデルが継続的かつ自動的なレビューを受け続けた経験を持つ設計者はほとんどいないだろう。モデルをインクリメンタルに、解析器を使って構築し、検査し続けるというのは、紙と鉛筆のみを用いるのとは大きく異なる経験である。最初は皆驚くだろう。即座で視覚的なフィードバックを受けると、モデリングははるかに楽しい。一部しかできていないモデルを解析すると、新たな制約を追加すべきと示唆する例が即座に返ってくる。 そして、痛みを伴うのは、自分が正しいことをほとんど何もしていないと分かったときである。自分が書き下したものは自分の意図を正確に表さない。仮に意図した通りになっていたとしても、それが期待した結果を得るとは限らない。自動解析ツールは人間のレビュワーよりもはるかに無慈悲である。

モデル検査の発明により、形式手法の評判は一夜にして変わったといっても過言ではない。「検証」（verification）という単語は再び流行のものとなり、チップメーカーでモデル検査ツールが採用され、エンジニアが現実に形式モデルを書けること、そしてその恩恵が大きければ、彼らは自発的にモデルを書くことが明らかになった。

「モデル検査」のススメ （ゲームシナリオ進行編）