Software Abstractions: Logic, Language, and Analysis（ソフトウェアの抽象：論理、言語、分析）

引用

Jackson, D. (2012). Software Abstractions: Logic, Language, and Analysis (revised ed.). MIT Press.

章の要約

本書（約 375 ページ）は、関係論理に基づくモデリング言語 Alloy と、モデルを自動的に検査する Alloy Analyzer を紹介する。主張は、ソフトウェア開発の核心は抽象の設計であり、コードは抽象を探るのに向いた媒体ではない、というものである。実行可能であることが無関係な細部を持ち込み、設計時には見えなかった欠陥がコーディング時に明らかになる。Alloy は表現しやすさを基準に選ばれた記法と、すぐに結果を返す分析を提供する。著者はこの方法を「軽量形式手法」と呼ぶ。伝統的な形式仕様のように小さく単純な記法を用いるが、定理証明の代わりに完全に自動の分析を行う。改訂版は本文、例、付録を Alloy 4 に合わせて更新している。第1章は短い導入、第2〜5章が言語の解説、第6章がより大きな例で、その後に五つの付録が続く。

第1章：はじめに

この章は、ソフトウェアは抽象の上に築かれること、検証していない抽象への希望的観測がよくある失敗の原因であること、その対策は分析可能な記法で抽象の設計に正面から取り組むことだと論じる。設計を独立した工程として廃する方法と対比している。

第2章：ひと通りの見学

住所録という拡張された例を段階的に組み立てる。この章は状態（静的な面）を探り、続いて操作（動的な面）、分類の階層、実行トレースを加え、細部に入る前に、シミュレートし、検査し、改良するという全体の流れを読者に示す。

第3章：論理

この章は言語の基礎にある論理を述べる。「三つの論理が一つに」、アトムと関係、スナップショット、演算子、制約、宣言と多重度制約、そして濃度と整数を紹介する。

第4章：言語

「自分自身の祖父」（self-grandpas）の例から始め、シグネチャとフィールド、モデル図、型と型検査、ファクト・述語・関数・アサーション、コマンドとスコープ、モジュールと多相性、整数と算術を説明する。

第5章：分析

この章は Analyzer の動作を利用者の側から説明する。スコープ完全な分析、インスタンス・例・反例、無制限の全称量化子の問題、スコープの選択と単調性である。序文は、Analyzer が制約を論理式（ブール制約）に変換し、既製の SAT ソルバに渡すと述べている。

第6章：例

より大きな四つのモデル。リング上のリーダー選出、ホテルの部屋の施錠、メディア資産管理、メモリの抽象である。

付録 A〜E

付録 A は演習で、論理の演習、単純なモデルの拡張、古典的なパズル、メタモデル、小規模な事例研究、自由課題の事例研究からなる。付録 B は言語リファレンス（字句の問題、文法、優先順位、意味論、型とオーバーロード、言語機能、関係式・整数式・ブール式）である。付録 C は Alloy カーネルの意味論、付録 D は図式記法、付録 E はホテル施錠の問題に即して他の手法（B、OCL、VDM、Z）と比較する。

主要概念

第1〜2章：抽象と作業の流れ

• ソフトウェアの抽象：本質的な形に還元された構造。本書は設計の核心と見る。
• 軽量形式手法：厳密な記法と完全に自動の分析を、段階的に築いていく方法。

第3〜4章：論理と言語

• 関係論理：集合と関係をモデルの唯一の構成材料とする。
• シグネチャとフィールド：モデルがオブジェクトの種類とそれらの間の関係を宣言する方法。
• ファクト、述語、関数、アサーション：モデルと主張を書くための制約の形式。
• コマンドとスコープ：Analyzer に何を実行・検査させるか、またどの範囲でか。

第5章：分析

• スコープ完全な分析：定められた大きさまでのすべての場合の網羅的な検査。
• インスタンスと反例：モデルの一例、またはアサーションの違反。視覚的に表示される。
• 無制限の全称量化子：無制限の集合にわたる量化子で、スコープを限った分析では完全にはカバーできない。5.3 節がこの問題を扱う。

批判的分析

長所

• 設計についての明快な主張。 序文と第1章が、抽象に早い段階で明示的に注意を払うべき理由を論じており、書名がその主題を示している。
• フィードバックを通じた学習。 序文は、Analyzer を使ってモデルを少しずつ作り、シミュレートと検査を繰り返し、即座に視覚的なフィードバックを得て、自分のモデルの誤りを見つけるという経験を描いている。
• 段階的な道筋。 ひと通りの見学が論理と言語の章より前にあるので、読者はまず作業の流れを目にする。付録には論理の演習から自由課題の事例研究まで六種類の演習がある。
• 詳細な事例とモデル。 第6章は四つのシステムをモデル化し、書籍サイトからはすべてのモデルをダウンロードできる。
• 書評。 George Hacken（『Computing Reviews』）は例と演習を評価して最高の推薦を与えた。Anthony Sloane（『Journal of Functional Programming』）は、Alloy のようなシステムはすべてのソフトウェア設計者・開発者の道具箱にあるべきだと書いた。

短所

• ツールのバージョン。 改訂版は Alloy 4 に対応している。Alloy のサイトには現在、時相モデリングなど Alloy 6 の機能を扱う新しいオンライン書籍『Practical Alloy』が挙がっている。
• 有界の分析。 この方法は定められたスコープまでのすべての場合を調べるので、検査を通ったモデルがあらゆる大きさで正しいと証明されるわけではない。第5章は無制限の全称量化子とスコープの選び方に節を割いている。
• 論理の素養が必要。 内容は集合、関係、一階論理に基づいており、離散数学に慣れた読者に向く。
• プログラムではなく設計のモデル。 モデルが記述するのはコードではなく設計である。他の仕様手法との比較は付録 E に限られ、そこではホテル施錠の問題で Alloy を B、OCL、VDM、Z と並べている。

コースにおける位置づけ

ソフトウェア工学の書目の中の形式手法の本である。『A Philosophy of Software Design』は、深いモジュールと情報隠蔽によって複雑さを管理する短い本で、Jackson と同様に抽象に関心を持つが、実用的な助言として表現している。『Software Architecture in Practice』は実際のプロジェクトにおけるアーキテクチャと品質特性を扱い、Sommerville の『Software Engineering』はシステムの全生涯を追う広い入門書、『The Pragmatic Programmer』は実践的な習慣の集成、『Software Engineering at Google』は大きな組織がどのようにソフトウェアを長く保つかを説明する。

ソフトウェア工学の全体像をつかんだうえで、作り始める前に設計を厳密に検査する方法がほしいときに『Software Abstractions』を読む。これらの実用書を置き換えるのではなく補うものである。

本書の使い方

集合、関係、一階論理に慣れ、ソフトウェア設計の経験が多少ある読者向けである。書籍サイトの推薦文は、実務家から研究者までの読者を想定している。

実用的な進め方：

• 最初の通読： 第1章、第2章の見学、言語の第4章。Alloy Analyzer をインストールし、サイトにある本のモデルを実行する。
• 中核： 第3章（論理）を第4章と並行して読み、続いて第5章で分析結果の読み方とスコープの選び方を学ぶ。
• 応用： 第6章のモデルを少なくとも一つ最後まで読み、変更してみる（ホテルの部屋の施錠は、付録 E が記法の比較に用いる問題でもある）。
• 練習： 付録 A の演習を、論理の演習から小規模な事例研究へと進めて行う。付録 B を言語リファレンスとして、付録 E を記法の比較に使う。