下限多重度someとone三項関係のセマンティクスは把握するのが困難です。Software Abstractions (Rev. ed.) pp.79-80 によると、関係は(p.97 も参照)addr: Book -> (Name -> some Addr)と同等である必要があります。all b: Book | b.addr in Name -> some Addrしかし、後者の式は正確には何を意味するのでしょうか? ここで私の想像力は失敗します。そのため、Alloy Analyzer 4.1.0 でいくつかの実験を行いました。このモデルでの含意:
sig Name, Addr {}
sig Book { addr: Name -> some Addr }
assert implication {
#Book = 0 or all n: Name | some b: Book, a: Addr | n in b.addr.a
}
check implication
成立します (反例は見つかりません)。そのため、Book が存在する場合、各 Name はそれらの Book の少なくとも 1 つに登録されている必要があります。文書化されていないアドレスは許可されており、ブックがなければ、文書化されていない名前も突然許可されているように見えます。
次のモデルでの含意:
sig Name, Addr {}
sig Book { addr: Name some -> Addr }
assert implication {
#Book = 0 or all a: Addr | some b: Book | #b.addr.a > 0
}
check implication
再び保持します。これは以前のモデルの鏡像です: Book がまったくない場合を除き、文書化されていない Addrs は禁止されています。また、名前の文書化に関する制約はありません。
両方のモデルを組み合わせて、より簡潔に定式化できます。
sig Name, Addr {}
sig Book { addr1: Name -> some Addr, addr2: Name some -> Addr }
assert implications {
some Book implies Name in Book.addr1.Addr and Addr in Book.addr2[Name]
}
check implications
したがって、Book がある場合、すべてのName がリレーション addr1 に参加し、すべてのAddr が addr2 に参加する必要があります。多重度は同様に動作します。one
下限制約に関する限り、ソフトウェア抽象化とアナライザーはR: A -> (B m -> n C)のような構造について同じ話をしていないようですが、何かを見落としている可能性があります。私が発見した意味は、私が期待していたものではありませんでした。私がまだ発見していない他の奇妙な意味があるかもしれません. ネストされた下限多重度はまったく意味をなさないとますます感じています。私はこれで正しいでしょうか？