0
以下は、電子メールアドレス帳の合金モデルです。アドレス帳の各名前は、名前またはアドレスのいずれかにマッピングされます。私のアサーションが実際にチェックしたいものをチェックしていることを確認するにはどうすればいいですか？
それぞれの名前を最終的にアドレスにマッピングする必要があります（例：Family - > Tom - > Tom_addr）。私はこれを実装するための事実を作りました。私の事実が正しいことを確認するために、私はアサルトを作成しました。
私はアサルトに何を配置するかについて長い間困惑していました。奇妙なことに、私が「事実」セクションに置いた表現は、アサルトに置く正しい表現のように思えます。しかし、その主張はただの事実を繰り返すだけであり、それは役に立たない。だから私は主張に置くべき何かを作った。
"assert"セクションに置かれたものが実際にはすべての名前が最終的にアドレスにマッピングされることを実際に確認しているとは確信していません。
質問：「事実」セクションで
は、私が正しく、それぞれの名前が、最終的アドレスにマップ制約を表明していますか？
"assert"セクションでは、すべての名前が最終的にアドレスにマップされることを示す良い方法がありますか？
sig Addr {}
sig Name {
address: some Addr + Name
}
fact {
// No cycles.
no n: Name | n in n.^address
// All names eventually map to an Addr.
// Here's how I implemented the constraint:
// There is no name n that is mapped-to (i.e., m -> n),
// which does not map-to something (i.e., n -> p).
no n: Name {
n in univ.address
n not in address.univ
}
}
assert All_names_eventually_map_to_an_Addr {
all n: Name | some n.^address & Addr
}
check All_names_eventually_map_to_an_Addr