Как смоделировать оператор по модулю в сплаве?
Я хочу попробовать сплав, чтобы доказать, что любое число, кратное 4, делится на 2....
Вот мой код..
//proof that 4n is divisible by 2
module I4nDivisibleby2
sig num {}
fact {
all n:num|n%4=0
}
assert even {
all n : num | n%2 = 0
}
check even for 1
Это не компилируется
Вы должны использовать функцию rem, определенную библиотекой. Функция rem принимает два целых числа, поэтому вы не можете вызвать ее для экземпляра num; вместо этого вы могли бы сделать что-то вроде
module I4nDivisibleby2
sig num {
val: Int
}
fact {
all n:num | rem[n.val, 4] = 0
}
assert even {
all n : num | rem[n.val, 2] = 0
}
check even // => no counterexample found
