抽象によるソフトウェア設計 序文、第1章「はじめに」

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

今日から「抽象によるソフトウェア設計−Alloyではじめる形式手法−」を読みます。形式手法によるソフトウェアの設計とそれを支援するツールAlloyを紹介する本、だと思います。Alloyも形式手法についてもまったく初めて触れるのでどんな内容なのかまだわかりません。今日はとりあえず序文と「はじめに」だけです。

• 「日本語版に寄せて」より "日本語への翻訳は、まるで形式化を行なうようで、不具合を確認するにはとても生産的な方法のようだ"
• 軽量形式手法 (Lightweight formal method)
  • モデルをインクリメンタルに開発する
  • 設計を表現するモデルを作って、それを解析器にかけるとおかしなところや抜けているところが指摘される、というものらしい
• 設計をシンプルに保つことの重要性
• 開発は直線的に進む*べき*
  • 最近流行りのアジャイルとは別の考えかたですね
  • うまくいかないのは、設計時の環境が厳密さにかけるため → ツールを用いて堅牢な設計を
  • XP は設計という独立したフェーズをなくしすぐにコードを実装する、とある
    • ただ XP (アジャイル？)が立ち向かうのは設計の困難さではなくて、要求が変化することだと思うので、この点はちょっと批判としては的外れと思われる
  • コードは抽象化された設計を記述するには不向き
• 形式仕様記述と静的解析
  • 数学的記法とツールの不足が障壁
• 定理証明によらず有限の解空間を探索する手法 → Alloy
  • lightweight で XP のような開発スタイルと親和性が高い
• 論理系、言語、解析

新しく勉強する分野なのでとてもワクワクします。第2章からはさっそくサンプルを動かすみたいなので環境を構築しないと。