[Rodin-b-sharp-user] errata in the Event-B book

[Matthias S. <Mat...@in...>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Dear Jean-Raymond,

I have recently come across some errata in your book:

Chapter 9:
- ----------
1) Cartesian products

I was unable to prove theorems of the form
"!x. x : S ** T => (#x1,x2. x1|->x2 = x)".
I think a rule is missing.

2) Integers

The expression "x = 1/(-1)" may be rewritten to
"#r. (r:NAT & r < -1 & 1=x*(-1)+r)". That allows you to rewrite a
satisfiable predicate into an unsatisfiable one. That can be used to
prove false.

Chapter 5:
3) I was playing around with proof obligations and got an example where
the tool produces a proof obligation differing from the specification in
the book. Of course, it could also be the case that Rodin is wrong, but
Rodin's proof obligation makes more sense to me then yours. The final
decision is up to you.

Here is the model:
machine ref_0

variables x

invariants
@inv1 x ∈ ℤ

events
  event INITIALISATION
  ...

  event evt0
  any a where
    @grd0 a > 0
  begin
    @act0 x ≔ x+a
  end
end

machine ref_1 refines ref_0

variables y

invariants
  @inv1 y ∈ ℤ
  @inv2 x = y

events
  event INITIALISATION
  ...

  event evt0 refines evt0
  with
    @a 1=a
  then
    @act0 y ≔ y+1
  end
end

According to your book the proof obligation evt0/inv2/INV should not
contain the witness "1=a", because it is the witness predicate for a
parameter and not for a variable. But the Rodin proof obligation does
contain the witness.
Rodin's proof obligation can be proved, yours cannot.
Rodin's proof obligation makes sense to me, because according to my
intuition and to your definition of refinement in Chapter 14 evt0 does
indeed refine evt0.

Cheers,

Matthias
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFMbUxsczhznXSdWggRAqapAKCe5T54QUe/skTR7SWAAJsJENGrZACgt63+
ZZflJqmrXZDk7aIDODlsB7A=
=InFC
-----END PGP SIGNATURE-----