抽象によるソフトウェア設計－Alloyではじめる形式手法－の誤植報告等

[hawaii]

田辺です。本書第１版第１刷について誤植と思われる箇所（３つ）がありましたので
この場をお借りして報告させて頂きます。
もともと見事にブラッシュアップされていたので、
読み進めていく上で支障があるものはありませんでした。


(1)--------------------------------------------------------------------------------

p.69

例：前の例と同じ集合および関係を考える。
all n: Name | lone n.address
は、「すべての名前は高々１つのアドレスに割り当てられる」ことを意味する（前の例より簡単な記法）。

→ この制約が本来意味するのは「すべての名前は高々１つのアドレスか名前に割り当てられる」
これは前の例と等価ではない。実際、以下のコードを実行すると反例が生成される。

-- 例：電子メールアドレスの集合 Address と、名前の集合 Name と、名前から名前また
--はアドレスへの割り当てを持つ階層的なアドレス帳を表す関係 address を考える。（p.68）
sig Address {}
sig Name {
address: set Name + Address
}

check {
all n: Name | lone d: Address | d in n.address
iff
all n: Name | lone n.address
}

(2)--------------------------------------------------------------------------------

p.133

module booleans
sig Boolean {}
one sig True, False extens Boolean {}

→ abstract sig Boolean {} だと思われる。
なお、ライブラリ util/boolean は abstract sig Bool {} と定義されている。

(3)--------------------------------------------------------------------------------

p.202 図 6.12

pred appInv (xs: ApplicationState) {
all cs: xs.catalogs | catalogInv (xs.catalogState[cs])
}

→ all cs: xs.catalogs | catalogInv [xs.catalogState[cs]]


********************************************************************************
※以下は、誤記報告ではありません。

ことのついでに本文に対する私なりの補足です。
他の方の参考になれば幸いです。

p.17
sig Book {addr: Name -> Target}
{ no n: Name | n in n.^addr }
→ p.18 と p.19 では、n.(^addr) となっているが、括弧はあってもなくてもよい。

p.80
しかし比較演算子は、その標準的な意味のままである。
→ これは等号に限った話。

p.99
Alloy解析器ではAlloyのテキストベースのモデルからモデル図を生成することができる。
→ メニュー Excecute → Show Metamodel を実行する。

p.132
6 Int
→ Alloy 4.1.10 使用の際は 6 int と指定。

p.142
Alloy解析器では、もっと普通の（多少はなじみやすい）フォーマットを関係の宣言から判断してテキスト形式での出力に使う。
→ テキスト形式の出力については次のトピックを参照。
http://groups.google.com/group/alloy-jp/browse_thread/thread/b5c0fddc837e1244#


以上です。
お時間のある際にご確認頂けると幸いです。

[Takeo Imai]

今井です。

ありがとうございます。実は誤植の報告下さったのは、（私が把握してる限り）田辺さんが初めてです。
ぱっと見る限り、いずれもご指摘の通りかと思われます。
原書の問題でもあるので、原著者とも相談します。

2011/11/6 hawaii <happy.lov...@gmail.com>:

--
IMAI Takeo <takeo...@gmail.com>