生成公理がない場合の検査について
happy love
生成公理にまつわる問題についてお尋ねします。
p150 の 5.3 非限定の全称限量子 では、「fact などで書かれる生成公理がない場合、操作結果の値の割当てが保証されない」というような
ことが書かれています。
そして、以下の検査で不思議な反例が生成されることが例示されています。
-- p155-156 の例より
sig Name, Addr {}
sig Book {
addr: Name -> Addr
}
pred add(b, b': Book, n:Name, a: Addr) {
b'.addr = b.addr + n -> a
}
assert AddTotal {
all b: Book, n: Name, a: Addr |
some b': Book | add [b, b', n, a]
}
check AddTotal --この検査で想定外の反例が生成される
このことを踏まえた上で疑問に思うことがあるのですが、
第１章の add の冪等性のアサーションでは、十分な検証を行えているのでしょうか。
-- p14 より
assert addIdempotent {
all b, b', b'': Book, n: Name, a: Addr |
add [b, b', n, a] and add [b', b'', n, a] implies b'.addr =
b''.addr
}
check addIdempotent for 3
というのも、公理なしでは操作結果の存在が保証されていないわけですから、
前提 add [b, b', n, a] and add [b', b'', n, a] を満たすタプルの組合せがひとつもない場合も考えられま
す。
その場合、このアサーションは add を複数回適用した結果をひとつもチェックせずに合格することになります。
前提を満たす組合せがあったとしても、思うより少ないかもしれません。
このような可能性については、どのように扱えばよいでしょうか。気にする必要はないでしょうか。
また、この検査で、実際に add [b, b', n, a] and add [b', b'', n, a] を満たしたタプルやケース数を確認
する何かよい方法はありますか。
Takeo Imai
2011/10/21 happy love <happy.lov...@gmail.com>:
> 第１章の add の冪等性のアサーションでは、十分な検証を行えているのでしょうか。
生成公理について、誤解があるように思います。
> assert AddTotal {
> all b: Book, n: Name, a: Addr |
> some b': Book | add [b, b', n, a]
> }
で不思議な反例が生まれる（と思ってしまう）のは、 全章限量された任意の b, n, a に対して b'
が「スコープ内に常に存在する」ことを暗に期待しているからです。
実際には、（b, n, a がスコープ内にあったとしても）b'
を満たすアトムがスコープ外にはみ出している可能性があり、その場合にAlloyでは反例が生成されてしまいます。
問題の
> assert addIdempotent {
> all b, b', b'': Book, n: Name, a: Addr |
> add [b, b', n, a] and add [b', b'', n, a] implies b'.addr =
> b''.addr
> }
の場合ですが、そのような現象は起こりません。必要な変数は全て全称限量されていて、予想外に何かがスコープ外にはみ出すことはないからです。
仮にですが、述語 add が
pred add(b, b': Book, n:Name, a: Addr) {
b'.addr = b.addr + n -> a
}
でなく
pred add(b: Book, n:Name, a: Addr) {
some b': Book | b'.addr = b.addr + n -> a
}
という形をしていて、検査したいアサーションが
assert addIdempotent' {
all b, b', b'': Book, n: Name, a: Addr |
add [b, n, a] and ...
となっていたら話は別です。このとき、add を展開した
all b, b', b'': Book, n: Name, a: Addr |
some b''': Book | b'''.addr = b.addr + n -> a and ...
で、b, addr, n, a らがスコープ内にあっても、b''' （展開時に名前付け替えました）
がスコープ外にはみ出している可能性があり、意図しない反例が出る可能性があります。
> また、この検査で、実際に add [b, b', n, a] and add [b', b'', n, a] を満たしたタプルやケース数を確認
> する何かよい方法はありますか。
数のカウントは難しいですが、検査とは別に、次のような述語を書いてシミュレーションしてみるのはどうでしょうか。（実際に動かしてないので、バグが入ってたらスミマセン）
pred test (b, b', b'': Book, n: Name, a: Addr )
add [b, b', n, a] and add [b', b'', n, a]
}
run test for 3
--
IMAI Takeo <takeo...@gmail.com>
Yamamoto Koji 山本晃治
生成公理を利用しなくても解析器が同じ結果を返すための規則として挙げ
られている限定全称規則についてです．
この規則の言う「限量変数の範囲式が生成シグネチャに言及しない」の
「言及」の意図 (原文の "mention the names" の意図) がくみとれません．
邦訳 p.155 の例 (集合和可換の表明) では全称限量子自体が現れないため，
言及の例にはなっていないんだと思います (限定の例にはなっていますが．)
どこかに例はないでしょうか．
--
山本晃治 <kouj...@pobox.com>
Yamamoto Koji 山本晃治
Yamamoto Koji 山本晃治 <kouj...@pobox.com> wrote:
> どこかに例はないでしょうか．
ちょっと自分で例を探してみました．
文献[46] "Relational Analysis of Algebraic Datatypes" の2章にある次
のアサーションが例になっている?
assert Deconstruct {
all c: Cons | some l: c.*rest, e: Element |
cons(e, l, c)
}
だとすると "(l is) bounded by an expression in terms of variables
bound in an outer quantifier" が「言及」の説明になってるんでしょう
か?
At Fri, 21 Oct 2011 11:14:46 +0900,
happy love
仰るとおり偽反例の現象を誤解してました。
ですが、結果値がスコープ外になってしまう可能性については認識していました。
結局、以下のように認識を整理して、addIdempotent の検査には問題ないことを理解しました。
(誤解) スコープ内に、生成公理を満たすインスタンスが見つからなかったため、偽反例が生成された。
(正解) 生成公理を満たさないインスタンスがスコープ内にあったため、偽反例が生成された。
以下、誤解に至った理由を補足させて頂きます。
提示した例に対して、コマンド
check AddTotal for exactly 2 Name, exactly 2 Addr, exactly 8 Book
をそのまま実行すると偽反例を生成しますが、以下の制約を追加して実行すると偽反例が生成されません。
fact {
some b': Book | add [b, b', n, a]
}
スコープ内で生成公理を満たすインスタンスが見つけられない、というように誤解してしまいました。
P.S.
質問文に誤りがありました。（質問自体が見当外れでしたが）
以下のように訂正させて頂きます。
(誤) 第１章の add の冪等性のアサーションでは、..
(正) 第２章の add の冪等性のアサーションでは、..
Takeo Imai
2011/10/21 Yamamoto Koji 山本晃治 <yamamot...@jp.fujitsu.com>:
> 文献[46] "Relational Analysis of Algebraic Datatypes" の2章にある次
> のアサーションが例になっている?
(snip)
> だとすると "(l is) bounded by an expression in terms of variables
> bound in an outer quantifier" が「言及」の説明になってるんでしょう
> か?
はい。まぁこれも、あまり正確な表現とも取りづらいですが、Alloy本に出てくる「限定全称規則」（bounded-universal
rule）の（ほぼ）正確な定義は、この文献[46]の4節 Definition 1 に出てくる EBU sentence のことです。
「範囲式が生成シグネチャに言及しない」というのは、内側の限量子が、外側の限量子の範囲式そのものを含まないことを意味しています。
外側の限量子の空間よりも内側の空間が常に小さくなるような式にすれば、（＋適切なスコープを選べば）ある有限のスコープ内に全てが収まる、というのが、限定全称規則のココロです。
これはおっしゃるとおりで、同じ要望を私たちも原著者のJackson教授に上げました。
Jackson教授もその点は認めておられたんですが、手間と時間の問題で、新たな例の加筆まで手が回らなかったというのが実情です。
--
IMAI Takeo <takeo...@gmail.com>
Koji Yamamoto
2011/10/21 Takeo Imai <takeo...@gmail.com>:
> Alloy本に出てくる「限定全称規則」（bounded-universal
> rule）の（ほぼ）正確な定義は、この文献[46]の4節 Definition 1 に出てくる EBU sentence のことです。
なるほど，この定義直前の bounded universal term quantifier の説明と合わせて，
ちょっと理解した気になりました．
> 「範囲式が生成シグネチャに言及しない」というのは、内側の限量子が、外側の限量子の範囲式そのものを含まないことを意味しています。
> 外側の限量子の空間よりも内側の空間が常に小さくなるような式にすれば、（＋適切なスコープを選べば）ある有限のスコープ内に全てが収まる、というのが、限定全称規則のココロです。
ありがとうございます．ちょっと取組中のモデルで限定全称規則に反しているところが
ないか確かめてみたくなりました．
そして限定全称規則を守った記述に対して (伝わるように言い表せないんですが) 例・反例が
見つかるように Alloy が「外側の空間」をうまく広げてくれるのかも確かめてみようかと．
# 上の一文は意味不明だと思うので読み流してください．
# ところで研究室から離れているので「このココロは何だ?」っていう「ココロ」の
# 言い回しを久しぶりに聞けました．
> At Fri, 21 Oct 2011 11:14:46 +0900,
> Yamamoto Koji 山本晃治 <kouj...@pobox.com> wrote:
> これはおっしゃるとおりで、同じ要望を私たちも原著者のJackson教授に上げました。
> Jackson教授もその点は認めておられたんですが、手間と時間の問題で、新たな例の加筆まで手が回らなかったというのが実情です。
そうなんですね．例えば web 上などで追加例が載る日が来るといいですねぇ．
とはいえ Alloy 本としてまとまっている現状だけでも，ずいぶんありがたいです．
# 使っていないのでよくは知りませんが，Event-B などだと記述のシンタックスと意味を
# 把握しきるだけでも大変そうなので...