1

名簿の例の次の単純な変形を考えてみましょう

sig Name, Addr {}
sig Book { addr : Name -> Addr } // no lone on Addr
pred show(b:Book) { some n : Name | #addr[b,n] > 1 }
run show for exactly 2 Book, exactly 2 Addr, exactly 2 Name

一部のモデルインスタンスでは、エバリュエーターで次の結果を得ることができます

all b:Book | show[b]
--> yields false
some b:Book | show[b]
--> yields true
show[Book]
--> yields true

showがリレーションだった場合、{true、false}のような答えが得られると期待するかもしれません。述語である場合、単一のブール値が返されます。show [Book]は、その上の全称記号表現の省略形であると期待していました。代わりに、存在記号を使用して結果を折りたたんでいるようです。誰もがこれの合理的な理由を知っていますか、またはshow [Book]の意味について別の説明がありますか？

4

1 に答える 1

1

(これについて正しい言葉を持っているかどうか確信が持てないので、あいまいに思われる場合はご容赦ください。)

個体を表す Alloy のすべての表現は個体の集合を表し、言語では「個体 X」と「個体 X をメンバーとする単一集合」の間に利用できる区別がないことに注意してください。([後の補遺:]より一般的に使用される用語: Alloy のロジックの一般的な規則は、すべての値が関係であるということです。シングルトン セットです。Software Abstractionsのセクション 3.2.2 の説明、またはGreg Dennis と Rob Seater による Alloy Analyzer 4 チュートリアルのスライド「Everything's a relationship」を参照してください。)

'show' 述語の宣言を考えると、'show' の引数が単一の Book (より正確には Book の単一セット) であることを期待するのは簡単です。引数が実際には (show[Book]ここでの式のように) シングルトン セットではない場合、システムはそれを強制的にシングルトン セットにするか、ある種の暗黙の存在または全称量化で解釈します。しかし、宣言pred show(b:Book) ...では、式b:Bookは署名 Book 内のオブジェクトのセットとなるオブジェクト b に名前を付けるだけです。(b が単一集合であることを要求するには、 と記述しpred show(one b: Book) ...ます。) の本体を構成する式showは、b = Book$0 と同様に、b = Book についても評価されます。

存在量化の出現は、式の中心にあるドット演算子addr[b,n](または同等n.(b.addr)に定義されている) の結果です。実際、実験すると、show[Book] が、 set of all books には、存在解釈が失敗する場合でも、2 つの異なるアドレスへのマッピングが含まれています. これをモデルに追加してみてください. たとえば:

pred hmmmm { show[Book] and no b: Book | show[b] }
run hmmmm for exactly 2 Book, exactly 2 Addr, exactly 2 Name
于 2013-02-01T22:23:31.807 に答える