Implication inside an Existential Quantifier: Difference between revisions

With version 1.15 ProB produces a warning if you use an implication inside an existential quantifier. Here we explain why.

Take a look at the following formula:

  f: 1..3 --> NAT &
  f = [0,0,0] &
  #i.(i:dom(f) => f(i)>0)

You may be surprised to learn that the existential quantifier on the third line is true, even though no element of the array f is greater than 0. Indeed, for i=0 or i=-1 or i=4 the body of the quantifier is true as i:dom(f) is false and hence the implication is true.

Usually, one intended to write a conjunction inside the quantifier, such as the following (which is now false given f=[0,0,0]):

  #i.(i:dom(f) & f(i)>0)

Note that in Atelier-B a top-level implication is not allowed inside an existential quantifier; one can only use a conjunction at the top-level. However, this may only displace the problem, as the following predicate is acceptable for Atelier-B but is semantically equivalent to the first existential quantifier above:

#i.(i:INTEGER & (i:dom(f) => f(i)>0))

Note that in particular in Rodin you can accidentally introduce an implication due to its subtly different priorities. Let us look at the next Event-B context (in Camille syntax):

context TestExistImplicationOrder
constants x y
axioms
 @axm1 x=1
 @axm2 y=2
 theorem @thm3_true ∃z·(z∈1‥3 ∧ x=z) ⇒ y=44  // surprisingly this formula is true
end

You may be surprised to see that @thm3_true is actually provable within Rodin. One may expect the predicate to be equivalent to x:1..3 = y=44 which is false. Rodin, however parses the formula as an existential quantifier with the implication inside the body. Hence, z=0 or z=4 are solutions to the existential quantifier and the predicate is true.

When adding additional parentheses, the predicate becomes false and probably corresponds to what we expected to write:

 theorem @thm4_false  (∃z2·(z2∈1‥3 ∧ x=z2)) ⇒ y=44  

ProB will now emit a warning for @thm3_true (but not for @thm4_false).

Note that this error is present in one of the solutions to the ABZ 2014 landing gear case study. After adding the check to ProB, two tests using files from that case study solution where failing due to the warnings. The culprit was the following invariant, which can also be found in the published article:

@inv2 ∃po·(po∈ PositionsDG∧ gear_extended_p(po)=FALSE ∧ gear_retracted_p(po)=FALSE) 
                ⇒
               door_open_p=PositionsDG×{TRUE}

The interpretation of Rodin of this invariant does not correspond to the intended meaning as described in the article (" we express an invariant to state that when a gear is partly-extended then all the doors are open."). This shows that the new warning in ProB is useful, and that the priority rules of Rodin can be misleading, in particular to persons used to the classical B syntax.