OCL constraints on mutator methods



Date view Thread view Subject view Author view

Tony Simons (A.Simons@dcs.shef.ac.uk)
Fri, 05 Apr 2002 16:41:22 +0100


Dear pUML, I'd like to determine the limits of what it is possible to assert about mutator methods in OCL. For example, from the published literature, I would think that the following is not allowed: context Stack inv: ------------------ push(e:Element).pop() == self because it involves mutator methods in the constraint expression. One could attempt to get around this locally by constructing the following const method of a Stack: bool Stack::isLIFO() const { Stack copy(self); copy.push(e); copy.pop(); return equals(copy); } and now write the OCL invariant: context Stack inv: ------------------ self.isLIFO() which locally doesn't modify anything in relation to the Stack self, but of course isLIFO() has to modify a copy of self. I believe that this also would not be allowed. If so, it seems that one is reduced to specifying operations only in terms of some postcondition on the underlying (eg) array representation of a Stack, as in Eiffel: context Stack::pop() --------------------- pre: not empty() post: size() + 1 == old size() although this may not be syntactically correct OCL, for which apologies (how do you refer to the old and new states of self? Is it self@pre.size(), or somesuch?) But the point is: can we not express postconditions in terms of abstract properties, rather than in terms of the representation? If this is so, then I think there may well be some problems in seeking to write properly abstract specifications. -- Tony ========================================================================== Dr Anthony J H Simons a.simons@dcs.shef.ac.uk Senior Lecturer in Computer Science http://www.dcs.shef.ac.uk/~ajhs Director of Teaching Department of Computer Science tel: (+44) 114 22 21838 University of Sheffield dept: (+44) 114 22 21800 Regent Court, 211 Portobello Street fax: (+44) 114 22 21810 SHEFFIELD, S1 4DP univ: (+44) 114 22 22000 United Kingdom ==========================================================================


Date view Thread view Subject view Author view