谓语用合金

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] }