[Apologies in case of multiple copies of this message]
Dear Professors and colleagues,
I have remarked in the following book
 Refinement in z and object-z: Foundations and
advanced applications . John Derrick and Eerke Boiten.
Formal Approaches to Computing and Information
Technology. Springer, May 2001
cases of examples, formulas, specifications and
refinement step that appeared before in other
publications (in my humble opinion):
 Desmond D'Souza, Alan Cameron Wills , Objects,
Components, and Frameworks with UML: The Catalysis(SM)
Approach, Addison-Wesley Professional October 19, 1998
 On the Verification of VDM Specification and
Refinement with PVS, Sten Agerholm, Juan Bicarregui
and Savi Maharaj, 1998, pp 157-189 of 
 On Verification of VDM Specification and
Refinement with PVS, Savi Maharaj and Juan Bicarregui,
1997. pp 280-289, proceedings of the 12th IEEE
International Conference in Automated Software
Engineering (ISBN: 0-8186-7961-1)
 "Proof in VDM: case studies" (ISBN 3540761861),
ed. Juan Bicarregui, Springer-Verlag, March 1998.
No citations, acknowledgements or errata are given.
Here are some examples (some pages from  are
attached, for honest informative purposes only) :
The formulas from the theorem 5.3.1 in , page 137,
are taken from . They are translated from OCL into
Z, using the very obvious correspondences of the
mathematical toolkits ( i.e AND translates into
Please compare the formulas from the theorem 5.3.1
with the following formulas from Catalysis :
page 266, section 18.104.22.168
'' If the requirement has several pre- and
postcondition pairs -
which may come from different supertypes - they
should be ANDed in
pairs ( (pre1 => post1) AND (pre2 => post2)) to
give an overall
requirement postcondition. If the pre- and
postconditions are not
from supertypes and are subject to joining
compose them accordingly."
page 324, section 8.2
Pre: inv & (pre1 | pre2)
Post: ((inv & pre A) => (post A & inv)) & ((inv & pre
B) => (inv & post
The same remarks apply to the reference  from ,
I have investigated these formulas for months and I
know they are not obvious at all.
The refinement of MSMIE protocol was investigated (for
the first time, to my knowledge) in  and . In
, this subject is presented like being introduced
by the authors, and it appears at pages
119-122, 125, 163-164, 170, 172.
The translations from VDM-SL into Z, used by the
authors of , are quit obvious: they take the
conjunction of pre and post conditions of the VDM_SL
specification and draw a Z box around.
In the Conclusions chapter of , page 440, there is
the only place where the book  is cited as
''Examples of refinement in VDM are given in …".
I would kindly ask you to check if my concerns are
Thank you very much!
Luggage? GPS? Comic books?
Check out fitting gifts for grads at Yahoo! Search
Received on Sun 03 Jun 2007 - 14:11:28 BST