From: Bujorianu Marius Constantin <*bujorianu_at_yahoo.com*>

Date: Sun, 3 Jun 2007 06:10:51 -0700 (PDT)

Message-ID: <20070603131051.65113.qmail@web37603.mail.mud.yahoo.com>

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

Date: Sun, 3 Jun 2007 06:10:51 -0700 (PDT)

Message-ID: <20070603131051.65113.qmail@web37603.mail.mud.yahoo.com>

[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 6.7.3.1 '' 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 B)) 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 correct! Thank you very much! Marius Bujorianu ____________________________________________________________________________________ Luggage? GPS? Comic books? Check out fitting gifts for grads at Yahoo! Search http://search.yahoo.com/search?fr=oni_on_mail&p=graduation+gifts&cs=bz

- application/pdf attachment: 1954143481-theorem.pdf

- application/pdf attachment: 794252599-MSMIE.pdf