[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Trying to figure out how theorems work with this basic example

The below module declares a set of numbers that are in the range 10 to 99 that are divisible by 2 only once and call it NumbersThatDivideBy2Once. At the end it declares a theorem that the constant input is a subset of NumbersThatDivideBy2Once.

--------------------------- MODULE TestModule ---------------------------
EXTENDS Naturals


Numbers == { n \in Nat : n > 9 /\ n < 100 }

DividesBy2(n) == (n % 2) = 0

DividesBy2Once(n) == DividesBy2(n) /\  ~DividesBy2(n \div 2)

NumbersThatDivideBy2Once == { n \in Numbers: DividesBy2Once(n) }

THEOREM input \subseteq NumbersThatDivideBy2Once


How can I check if this theorem holds for a given input? If I run a model check with a provided set of numbers as input, even if some of those numbers are not part of NumbersThatDivideBy2Once I still get no errors.

I've asked this question already on SO, without answers: https://stackoverflow.com/questions/53671776