謂語用合金

Question

參數和謂語不帶參數的，我看到一本書如下定義：

pred show(b: Book){ 
    some b.addr 
} 

其中

abstract sig Name, Addr {} 
sig Book { addr: Name lone -> lone Addr } 

與合金分析儀打後，我意識到這是一樣的

pred show(){ 
    some b:Book | some b.addr 
} 

我很好奇指定Book作爲參數的優點是什麼，而不是使用t他使用量詞的第二種方法？

Answer 1

使用或不使用參數給謂詞不是一種'方法'它有不同的語義。如果您在您的謂詞無法使用all b在它之外some b ...

例如：

sig Addr {} 

sig Book { 
    addr: Addr 
} 

pred show { 
    some b:Book | some b.addr 
} 

pred show'[b:Book] { 
    some b.addr 
} 

check { show } 

// These are not possible without an argument to show' 
check { all b:Book | show'[b] } 
check { some b:Book | show'[b] } 
check { no b:Book | show'[b] }