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)

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.

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 pitfall is present in one of the solutions to the ABZ 2014 landing gear case study. After adding the check for implications inside existential quantifiers to ProB, two tests using files from that case study solution were failing due to the new 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 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."). We were also initially surprised and suspected that ProB had erroneously generated the warnings. But it turns out that the warning is correct and useful, and that the priority rules of Rodin can 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.