1
Vote

During module instantiation, a module variable is bound to the wrong term (2015-03-07)

description

At line 272 in the file NewBoundedBuffer occurs the proof step:
 <2> (a (+) 1) (-) b = (a (+) 1) (+) OMinus(b)
      BY OMinusDef, Z3 DEF ZN
which expands to the obligation:
ASSUME NEW CONSTANT Msg,
       ...
       ASSUME 2 * NatInductiveDefConclusion \in Nat \ {0} 
       PROVE  \A a_1, b_1 \in 0..2 * NatInductiveDefConclusion - 1 :
                 a_1 (-) b_1 = a_1 (+) OMinus(b_1) 
PROVE  (a (+) 1) (-) b = a (+) 1 (+) OMinus(b)
The theorem OMinusDef is defined in the file IntegersModN.tla as:
THEOREM OMinusDef == \A a, b \in ZN : a (-) b = a (+) OMinus(b)
and in there, ZN is defined as:
ZN == 0..(N-1)
Since IntegersModN is instantiated via:
INSTANCE IntegersModN WITH  N <- 2*N
we would expect the obligation to contain 0..2*N-1, not 0..2*NatInductiveDefConclusion-1.

file attachments

comments