Сказуемое с аргументами и сказуемое без аргументов в сплаве

Я видел следующее определение в книге:

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

куда

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

Поиграв с анализатором Alloy, я понял, что это то же самое, что

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

Мне было любопытно, в чем преимущество указания Book в качестве аргумента, а не использования второго подхода с использованием квантификаторов?


alloy
person Programmer    schedule 16.11.2012    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Использование или неиспользование аргументов для предикатов не является «подходом», у него другая семантика. Если вы включите some b в свой предикат, вы не сможете использовать all 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] }
person Aviad P.    schedule 16.11.2012
comment
Утверждение второго check действительно эквивалентно show. - person afsantos; 22.02.2013
comment
Я также добавлю, что использование аргументов позволяет (более легко) проверять важные свойства. Например: правильность и согласованность операций. - person afsantos; 22.02.2013