Как проверить эквивалентность двух предикатов?

У меня есть две разные реализации для определенного предиката, и я хочу проверить, возвращают ли они оба один и тот же экземпляр, как я могу этого добиться?

Спасибо.


alloy
person Jack Stevens    schedule 15.11.2013    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Я бы утверждал, что два предиката всегда либо оба истинны, либо оба ложны, и проверял утверждение.

pred P1 { ... }
pred P2 { ... }
assert P1_equiv_P2 { P1 iff P2 }
check P1_equiv_P2

Если предикаты принимают аргументы, то конечно нужно проверять их на одних и тех же аргументах:

pred P1[x : univ] { ... }
pred P2[x : univ] { ... }
assert P1_equiv_P2 { all x : univ | P1[x] iff P2[x] }
check P1_equiv_P2
person C. M. Sperberg-McQueen    schedule 15.11.2013
comment
Спасибо, отличный ответ! - person Jack Stevens; 06.12.2013