Alloyで形式手法を学ぶ本「抽象によるソフトウェア設計」

ソフトウェア開発 UML 本

UMLの図面を描いていてもどかしく感じるのは、モデルで表現された概念が本当に矛盾・モレ無く実行可能なのか確信を持てない点だと思う。シーケンス図やステートマシン図なら動的な振る舞いを示すものなので理解しやすいし、動作をシミュレーションできるツールも有るけれど、検証しているわけではないから「ある特定の条件下では失敗する」ケースなんて、なかなか読み取れない。充分な経験を積んだ開発者がモデルの良し悪しをコメントしてくれるなら有難いものの、そんな人がいない職場も珍しくないし、そもそもそのような属人性に頼る開発も好ましくないように感じる。

そんな中、形式手法のAlloyについて書かれた本が出版されたので目を通してみた。Alloyは全くの初心者なので警戒していたのは事実だけど、（細かな文法はともかくとして）内容的には容易に理解できるもので、それほど難しくないことが分かった。著者の言う「軽量形式手法」が「従来の形式手法の恩恵をより低コストで得ようとするもの」を目指すという考え方も納得できるような気がする。もちろん、開発の実践に投入できるようになるまでにそれなりの訓練が必要とは言え、テキストで記述したモデルの概念がAlloyのツールにより図面で表現されて、望まない性質が検出された時には「反例」として明示してくれる。これなら誰にでも同じようなレベルでモデルの検証が出来そうだ。

この類の本では無味乾燥な文法に関する説明が延々と続くので読んでいて眠くなってしまうことが多いが、この書籍に限って言えば冒頭の「第2章 ざっと一巡り」でAlloyによる検証の全体像が紹介されているので、どのような仕組みなのかという点が分かり非常に理解しやすい。まずは、ここだけでも読んでみるべきだろう。また、初学者がハマリそうな落とし穴や、疑問に思うような些細なポイントも親切に説明されているので、なかなか良い参考書だと思う。著者の大学の教育者としての経験だけではなく、産業界でのコンサルティング経験も上手く反映されているようで、ソフトウェア設計にかける情熱のようなものが伝わってくる本でもあったりする。

APIの呼び出しをガシガシと書き並べるようなソフトウェア開発は、今日の開発現場の仕事としては必要だけど、そのような即物的な知識は実は陳腐化しやすい。そこから一歩視点を上げて、より抽象化したレベルで物ごとを考えられるようになると、ソフトウェアの信頼性は増すし、長期的に応用も効くようになる。そんな考え方を学ぶための本としてもお勧めだ。

しかしながら、自分の書いたモデルが継続的かつ自動的なレビューを受け続けた経験を持つ設計者はほとんどいないだろう。モデルをインクリメンタルに、解析器を使って構築し、検査し続けるというのは、紙と鉛筆のみを用いるのとは大きく異なる経験である。最初は皆驚くだろう。即座で視覚的なフィードバックを受けると、モデリングははるかに楽しい。

この章で見たような問題を、些細ですぐに気がつくものだと切り捨てるのはたやすい。実際に些細な問題であることも少なくないが、それは後から思い返したときにそう見えるだけだ。ソフトウェアの設計において最も困難でやりがいのあるチャレンジは、大量の複雑でつじつまの合わない詳細を、単純で汎用性のある概念へと還元することである。単純さは優れたソフトウェア設計の要なのである。

抽象によるソフトウェア設計−Alloyではじめる形式手法−

抽象によるソフトウェア設計−Alloyではじめる形式手法−

なお、UMLツールとしてお馴染みのEnterprise Architectにはアドインが用意されていて、クラス図を描くとAlloyの記法に出力してくれるという便利な機能がある。こちらも併せて使うと、より効率的な作業が出来ると思う。

形式手法というキーワードを聞いたことがあるが、どのようなメリットがあるのか、ということを知ることができるという意味では、Alloy Analyzerは事前の設定も不要で、図が表示されるのでわかりやすいなど多くの利点があります。

http://uml.livedoor.biz/archives/51562560.html

以下、Enterprise Architect連携機能を利用する場合の手順の紹介です。

http://uml.livedoor.biz/archives/51562895.html


関連