Implication inside an Existential Quantifier

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)

Maybe you are surprised 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. Quite often, existential quantifiers with a top-level implication are vacuously true. Hence, usually, one intended to write a conjunction inside the quantifier, such as the following formula (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))

ProB will also issue a warning for this slightly "hidden" implication.

In Rodin one can accidentally introduce an implication inside an existential quantifier, because the operator priorities of the implication and exists symbol can be surprising. 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. (See also page 11 of The Event-B Mathematical Language by Métayer and Voisin.)

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 new warning is triggered for invariant inv2 in one of the solutions to the ABZ 2014 landing gear case study:

@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 of the authors as described in the article (" we express an invariant to state that when a gear is partly-extended then all the doors are open."). Hence, the new warning by ProB is correct and useful. The priority rules of Rodin can thus be misleading, in particular to persons used to the classical B syntax.

Note: the case study has now been corrected and all invariants are proven and no events had to be changed. The corrected invariant simply moves the parentheses around the existential quantifier:

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