No edit summary |
No edit summary |
||
| Line 17: | Line 17: | ||
#i.(i:dom(f) & f(i)>0) | #i.(i:dom(f) & f(i)>0) | ||
</pre> | </pre> | ||
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: | |||
<pre> | |||
#i.(i:INTEGER & (i:dom(f) => f(i)>0)) | |||
</pre> | |||
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): | |||
<pre> | |||
context TestExistImplicationOrder | |||
constants x y | |||
axioms | |||
@axm1 x=1 | |||
@axm2 y=2 | |||
theorem @thm3_true ∃z·(z∈1‥3 ∧ x=z) ⇒ y=44 // suprinsingly this formula is true; see invariant in Mammar/Laleau landing gear model | |||
theorem @thm4_false ¬( (∃z2·(z2∈1‥3 ∧ x=z2)) ⇒ y=44 ) | |||
end | |||
</pre> | |||
You may be surprised to see that @thm3_true is actually provable within Rodin. | |||
One may expect the predicate to be equivalent to <tt>x:1..3 = y=44</tt> which is false. | |||
Rodin, however parses the formula as an existential quantifier with the implication <b>inside</b> 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: | |||
<pre> | |||
theorem @thm4_false (∃z2·(z2∈1‥3 ∧ x=z2)) ⇒ y=44 | |||
end | |||
</pre> | |||
ProB will now emit a warning for @thm3_true (but not for @thm4_false). | |||
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
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 false for f=[0,0,0]</ff>):
#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 // suprinsingly this formula is true; see invariant in Mammar/Laleau landing gear model theorem @thm4_false ¬( (∃z2·(z2∈1‥3 ∧ x=z2)) ⇒ y=44 ) 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 end
ProB will now emit a warning for @thm3_true (but not for @thm4_false).