Revisiting Feasibility POs - Revision history

imported>Laurent: Changed conclusion in the light of Rodin 2.3 implementation.

2012-01-30T18:33:53Z

Changed conclusion in the light of Rodin 2.3 implementation.

← Older revision		Revision as of 18:33, 30 January 2012
Line 112:		Line 112:
	hypotheses. We therefore have the same circular argument appearing again.		hypotheses. We therefore have the same circular argument appearing again.

	In summary, both the abstract before-after predicate and the witness must not		In summary, it appears that, in the general case, both the abstract
	put in hypothesis of any concrete feasibility proof obligation.		before-after predicate and the witness must not put in hypothesis of any
			concrete feasibility proof obligation.

	==Possible Solutions==		==Possible Solutions==
Line 137:		Line 138:
	obligation.		obligation.

	~~Such constraints would not hinder expressivity of~~ the ~~Event-B notation, as any~~		This is actually what is implemented in the proof obligation generator of Rodin
	~~occurrence~~ of ~~a concrete after value could be replaced with a fresh parameter~~		2.3. So, it is valid in this release to introduce the abstract before-after
	~~of the concrete event, and the before-after predicate of this variable moved to~~		predicate, as far as no parameter witness contains any after-value.
	~~a guard (possibly adding more fresh parameters for the after values of the~~
	~~other variables in the frame of the same action)~~. ~~This additional guard would~~
	~~not constrain more the concrete event~~, ~~as the existence of the fresh parameters~~
	~~with such properties~~ is ~~a logical consequence of the other guards (~~this
	~~corresponds~~ to the ~~feasibility proof obligation of the concrete actions~~ before
	~~changing them)~~.

	As concerns the witness for after values of abstract variables, we can get the		As concerns the witness for after values of abstract variables, we can get the
Line 187:		Line 182:
	In summary, both the abstract before-after predicate and the witness hypothesis		In summary, both the abstract before-after predicate and the witness hypothesis
	must be dropped from both the well-definedness and feasibility proof		must be dropped from both the well-definedness and feasibility proof
	obligations of concrete actions. ~~It could be~~ possible to ~~reintroduce them~~		obligations of concrete actions. However, if no parameter witness contains
	~~later, but this would need an overhaul of~~ the ~~proof obligation generator,~~		any after value, it is possible to introduce the abstract before-after predicate
	~~which could be carried through only~~ in ~~a major release of the Rodin platform~~		in hypothesis.
	~~(e.g., Rodin 3.0)~~.

	[[Category:Design]]		[[Category:Design]]
	[[Category:Work done]]		[[Category:Work done]]

imported>Laurent: Fixed several shortcomings of the previous version and reached a new conclusion.

2012-01-29T15:05:23Z

Fixed several shortcomings of the previous version and reached a new conclusion.

Show changes

imported>Laurent: Various typos fixed + new section on WD

2012-01-29T13:56:12Z

Various typos fixed + new section on WD

@@ Line 64: / Line 64: @@
        v' = 1                  // abstract before-after predicate
-       −(w' * w') = v'         // witness
+       v' = −(w' * w')         // witness
    |-  ∃ w' · w' * w' = −1     // feasibility predicate
-where the abstract before-after predicate has been applied as a substitution to the witness.
+where the witness (which is deterministic) has been applied as a substitution
 This proof obligation is easily discharged by instantiating the existential
@@ Line 74: / Line 75: @@
 From this example, the flaw in the proof obligation comes from the presence of
 the two hypotheses together.  If we remove any of them, then the proof
-obligation becomes unprovable, as expected.  So, we need to remove one of these
+obligation becomes unprovable, as expected.  So, we need to remove at least one
-hypotheses to make the <tt>FIS</tt> PO correct.
+of these hypotheses to make the <tt>FIS</tt> PO correct.
 ==A Bit of History==
@@ Line 92: / Line 93: @@
 The idea backing this change was to try to allow users to reuse somehow the
-<tt>FIS</tt> proof already carried on for the abstract actions when proving
+feasibility proof already carried on for the abstract actions when proving
 feasibility of the concrete actions.  For this, the POG adds one hypothesis
 which corresponds to the feasibility predicate already proved in the
@@ Line 143: / Line 144: @@
 out the witness does not loose any expressivity and is indeed much simpler.
-==About Well-Definedness of Actions==
+==Similar Proof Obligation==
 Looking at the code of the proof obligation generator, it appears that the
@@ Line 151: / Line 152: @@
 hypothesis can introduce inconsistency.  Following the same reasoning, it is
 decided to also drop the witness from <tt>WD</tt> proof obligations.
 ==Conclusion==

imported>Laurent: Initial complete version

2012-01-25T16:24:24Z

Initial complete version

New page

{{TOCright}}

==The Issue==

Son recently reported a
[https://sourceforge.net/tracker/?func=detail&aid=3469348&group_id=108850&atid=651669 bug]
in the Proof Obligation Generator (POG) of Rodin 2.3 where one could have
an event-B project containing two machines where all proof obligations are
discharged automatically although the concrete machine contains invariant
<math>\bfalse</math>. This is not something expected so some proof obligations
must be wrong.

==Analysis==

Looking more closely at the example attached to the bug, it appears that the
initialisation of the concrete machine is magic. It is therefore normal that it
can establish a <math>\bfalse</math> invariant. However, the feasibility proof
obligation <tt>FIS</tt> is supposed to work as a filter and prevent models from
containing magic actions. In the example, the <tt>FIS</tt> proof obligation of
the concrete initialisation is easily discharged and thus does not play its
filter role. This proof obligation is therefore wrong and needs to be fixed.

In a nutshell, the example attached to the bug, can be reduced to the
following. Take a machine M with the following contents

MACHINE
M
VARIABLES
v
INVARIANTS
inv1: v = 1 not theorem
EVENTS
INITIALISATION: not extended ordinary
THEN
act1: v :∣ v' = 1
END
END

and a concrete machine N refining M such as

MACHINE
N
REFINES
M
VARIABLES
w
INVARIANTS
inv1: v = −(w * w) not theorem
EVENTS
INITIALISATION: not extended ordinary
WITH
v': v' = −(w' * w')
THEN
act1: w :∣ w' * w' = −1
END
END

In Rodin 2.3, the <tt>FIS</tt> PO generated for the action of the initialisation of N is

−(w' * w') = 1
|- ∃ w' · w' * w' = −1

which is a contraction of the theoretical proof obligation

v' = 1 // abstract before-after predicate
−(w' * w') = v' // witness
|- ∃ w' · w' * w' = −1 // feasibility predicate

where the abstract before-after predicate has been applied as a substitution to the witness.

This proof obligation is easily discharged by instantiating the existential
quantifier of the goal with <math>w'</math>.

From this example, the flaw in the proof obligation comes from the presence of
the two hypotheses together. If we remove any of them, then the proof
obligation becomes unprovable, as expected. So, we need to remove one of these
hypotheses to make the <tt>FIS</tt> PO correct.

==A Bit of History==

In [http://www.event-b.org/abook.html Jean-Raymond Abrial's book], the
feasibility PO does not contain any of these hypotheses. It was also the case
in early versions of the Rodin platform. Looking at the code history, it
appears that the faulty hypotheses were added in commit r2786 of Tue Jan 9 2007
with comment
<blockquote>
Changed structure of generated POs.<br/>
The POG now tries to put feasibility of abstract actions in the hypothesis of
refined event actions. As a consequence the guard strengthening PO is now
stronger.
</blockquote>

The idea backing this change was to try to allow users to reuse somehow the
<tt>FIS</tt> proof already carried on for the abstract actions when proving
feasibility of the concrete actions. For this, the POG adds one hypothesis
which corresponds to the feasibility predicate already proved in the
abstraction together with the witness that describes the link between the
abstract and concrete actions.

On the one hand, there is no problem with the feasibility predicate of the
abstraction as it has already been proved in the abstraction under a more
restricted set of hypotheses (e.g., the concrete guards were not present).

On the other hand, stating also the witness that links after values of abstract
and concrete variables introduces a circular reasoning, as the witness supposes
that after values of concrete variables do exist, which is the exact meaning of
the feasibility proof obligation. We are thus left with a proof obligation to
demonstrate the existence of something, assuming that this something already
exists!

In summary, the witness linking abstract and concrete after-values must not be
put in hypothesis of any <tt>FIS</tt> proof obligation.

==Possible Solutions==

Introducing the abstract feasibility predicate in hypothesis was a good idea, a
priori. But if we cannot use the witness with it, is it still worth? Could we
put another hypothesis that would link the abstract and concrete after states?

Looking more closely at the problem, we can get the following insight: the
purpose of the witness is to describe how one can compute abstract after values
from concrete ones. It is the purpose of the <tt>WFIS</tt> proof obligation to
demonstrate that this computation is actually feasible.

However, in the case of the feasibility proof obligation, we need to go in the
opposite direction: we know that we have abstract after values and we want to
show the existence of concrete ones. We therefore want to use the witness in
the opposite direction. And no proof obligation is generated to show that the
witness can indeed be use in this opposite direction.

So, we have two possibilies for fixing the feasibility proof obligation:

# Either we keep the witness as hypothesis, but we generate a new proof obligation to show that the witness can be used to compute concrete after values from abstract ones.
# or we get rid of the witness in the feasibility proof obligation.

The first solution looks a bit heavy, as feasibility is the only place where
the witness is used in the direction from abstract to concrete. In all other
proof obligations, it is used from concrete to abstract. Therefore, introducing
a new proof obligation just for this is not worth it.

In the second solution, during proof, one can always state again the witness,
prove that it is invertible and then use it to achieve the proof. So leaving
out the witness does not loose any expressivity and is indeed much simpler.

==About Well-Definedness of Actions==

Looking at the code of the proof obligation generator, it appears that the
well-definedness (<tt>WD</tt>) proof obligation for concrete actions also has
both the abstract before-after predicate and the witness in hypothesis. So
this proof obligation is also erroneous as we've seen that this combination of
hypothesis can introduce inconsistency. Following the same reasoning, it is
decided to also drop the witness from <tt>WD</tt> proof obligations.

==Conclusion==

Therefore the witness hypothesis must be dropped from both the well-definedness
and feasibility proof obligations of concrete actions. The before-after
predicate of the abstract actions is still generated as hypothesis, as it can
be useful even when the witness is not present.

[[Category:Design]]
[[Category:Work done]]