Alloy在謂詞謂詞檢查中可能不一致的行爲？

Question

道歉的任何新手錯誤 - 這是我第一次在這裏發佈。

我不確定這是一個錯誤，還是Alloy合金類型檢測中某些微妙的結果。在下面的例子中，我認爲謂詞「奇怪」是不一致的，因爲B和C是不相交的集合。但是，Alloy（版本4.2）聲稱可以找到謂詞的模型。它顯示的模型看起來不對。例如，有一個模型只包含一個原子B $ 0，標記爲證人$ strange_a。在這個模型中，評估者告訴我isB [B $ 0]爲真，並且isC [B $ 0]給我一個類型錯誤，如預期的那樣。然而，奇怪的[B $ 0]評估爲真。我使用的合金代碼是：

abstract sig A {} 

sig B, C extends A {} 

pred isB [b:B] { } 

pred isC [c:C] { } 

pred strange [a:A] {isB[a] and isC[a]} 

run strange 

Answer 1

你說得對：這很令人驚訝。 Alloy的類型檢查器使用謂詞和函數的decl來檢查它們的body，但除了謂詞或函數在頂層運行時，它不會將它們強加爲約束。我們這樣做是因爲我們無法在所有用法上下文中找到這些約束的連貫語義（例如，在量詞內部或在否定下調用謂詞時）。