いくつか誤植と思われるものを発見しました

[Takuya Hitomi]

こんにちは。人見琢也といいます。

抽象によるよるソフトウェアを読んでいくつか誤植と思われる箇所と、

読んでいてよくわからない箇所があったのでリストにしてまとめました。

ファイルを添付しますので、

確認よろしくお願いします。

[Takeo Imai]

訳者の今井です。

人見さん、どうもありがとうございます。
ざっと見させていただきましたが、誤植・間違いの指摘は（著者にも確認しますが、現段階で
判断する限り）全部そのとおりかと思います。ありがとうございます。
# OCLの記述の中までよく目を通していただきました……

質問が２つあったと思いますが、これは明日以降回答させてください。
いや、今日はもう眠くなってしまったもので……^^;

> --
> このメールは Google グループのグループ「Alloy-jp」に登録しているユーザーに送られています。
> このグループから退会し、グループからのメールの配信を停止するには alloy-jp+u...@googlegroups.com
> にメールを送信してください。
> その他のオプションについては https://groups.google.com/d/optout にアクセスしてください。



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

[Takeo Imai]

今井です。頂いてた２つの質問にお答えします。

> 175ページ 議論のリング上のプロセスは常に識別子の大小の順にならんでいるの？の内容がわかりにくい。
> プロセスにP0 → P1 → P2 のように特定の順序を入れても一般性を失わないというのはわかるが、そ
> の次のsucc に制約を課すというのがわからない。succ に課される制約とは何なのか？ next に制約が
> 課されるのはわかるが、succ に制約を課してすべての状態が網羅されるのか？

うーん、これについては、私は本に書かれている以上の説明能力を持たないです。
succ に課される具体的な制約の内容を示せればよいのですが。原著者に聞いて
みるなりして、もう少し調べてみます。


> 225ページ A1.10 の不変条件(b) においてすべての名前は最終的にアドレスに対応づけられるが成り立つな
> らすべてのグループは空ではないが成り立ち、(d) のいくつかのグループは空ではないは常に成り立つ
> ように思うが、グループが空とはどのようなことを意図しているのか？

「すべての名前は最終的にアドレスに対応づけられるが成り立つならすべてのグ
ループは空ではないが成り立」つ、とは言えないと思いますよ。

例えばシグネチャAに対して

all a: A | ....

という制約があったとき、AlloyではAが空の場合もこの式は成り立ちます（....
の部分がなんであれ、常に真になります）。

試しに、(d)の代わりに「全てのグループは空である」というような制約を入れ
てみてください。インスタンスが出るはずですが、いかがでしょうか。

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

[Takuya Hitomi]

人見です。

回答頂きありがとうございます。

> うーん、これについては、私は本に書かれている以上の説明能力を持たないです。 
> succ に課される具体的な制約の内容を示せればよいのですが。原著者に聞いて 
> みるなりして、もう少し調べてみます。 

了解しました。おそらく紙面の都合上と、専門的になりすぎるので、

対称性破壊に関する細かい話を省いて、そのうえで説明しようとした結果、

この節の話が全体的にわかりにくくなっているのかもしれませんね。

> 「すべての名前は最終的にアドレスに対応づけられるが成り立つならすべてのグ 
> ループは空ではないが成り立」つ、とは言えないと思いますよ。 
> 
> 例えばシグネチャAに対して 
> 
>   all a: A | .... 
> 
> という制約があったとき、AlloyではAが空の場合もこの式は成り立ちます（.... 
> の部分がなんであれ、常に真になります）。 
> 
> 試しに、(d)の代わりに「全てのグループは空である」というような制約を入れ 
> てみてください。インスタンスが出るはずですが、いかがでしょうか。 

わかりました。Aliasだけのインスタンスが存在するんですね。

この問題を解いている時にその発想が出ませんでした。

お手数おかけしました。

ありがとうございました。

2014年8月27日水曜日 8時01分33秒 UTC+9 Takeo Imai: