Authorship questions

Authorship questions

From: Bujorianu Marius Constantin <>
Date: Sun, 3 Jun 2007 06:10:51 -0700 (PDT)
Message-ID: <>
[Apologies in case of multiple copies of this message]

Dear Professors and colleagues,

I have remarked in the following book

[1] 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): 

[2] Desmond D'Souza, Alan Cameron Wills , Objects,
Components, and Frameworks with UML: The Catalysis(SM)
Approach, Addison-Wesley Professional October 19, 1998


[3] On the Verification of VDM Specification and
Refinement with PVS, Sten Agerholm, Juan Bicarregui
and Savi Maharaj, 1998, pp 157-189 of [5] 


[4] 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) 


[5] "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 [1] are
attached, for honest informative purposes only) : 

The formulas from the theorem 5.3.1 in [1], page 137,
are taken from [2]. They are translated from OCL into
Z, using the very obvious correspondences of the
mathematical toolkits ( i.e AND translates into
\wedge, etc.).


Please compare the formulas from the theorem 5.3.1
with the following formulas from Catalysis [2]:


page 266, section


'' 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 [23] from [1],
dated 1999.

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 [4] and [3]. In
[1], 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 [1], 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 [1], page 440, there is
the only place where the book [5] 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!



Marius Bujorianu 

Luggage? GPS? Comic books? 
Check out fitting gifts for grads at Yahoo! Search

Received on Sun 03 Jun 2007 - 14:11:28 BST