Alloyで形式手法を学ぶ本「抽象によるソフトウェア設計」 - rabbit2goのブログUMLの図面を描いていてもどかしく感じるのは、モデルで表現された概念が本当に矛盾・モレ無く実行可能なのか確信を持てない点だと思う。シーケンス図やステートマシン図なら動的な振る舞いを示すものなので理解しやすいし、動作をシミュレーションできるツールも有るけれど、検証しているわけではないから「ある特定の条件下では失敗する」ケースなんて、なかなか読み取れない。充分な経験を積んだ開発者がモデルの良し悪しをコメントしてくれるなら有難いものの、そんな人がいない職場も珍しくないし、そもそもそのような属人性に頼る開発も好ましくないように感じる。 そんな中、形式手法のAlloyについて書かれた本が出版されたので目を通してみた。Alloyは全くの初心者なので警戒していたのは事実だけど、（細かな文法はともかくとして）内容的には容易に理解できるもので、それほど難しくないことが分かった。著者の言う「軽量形式手法」が「
