Re: OCL constraints on mutator methods



Date view Thread view Subject view Author view

Jos Warmer (J.Warmer@klasse.nl)
Tue, 09 Apr 2002 09:54:01 +0200


Tony, At 04:41 PM 4/5/2002 +0100, Tony Simons wrote: >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. This is correct. >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. This is "on the edge". No nexisting object has changed and there are no references made to the new object. You could even destroy the new object before returning the result.. >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() This doesn't look like a reference tom an array. It only tells me that the size of the stack has grown. >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? I would write additionally: context Stack::push(Object obj) post: size() = size@pre() + 1 post: top() = obj This captures only part of what you are trying to do. >If this is so, then I think there may well be some >problems in seeking to write properly abstract >specifications. It seems there are. >-- Tony Jos _____________________________________________________ Klasse Objecten tel : +31 (0)35 6037646 Chalonhof 153 fax : +31 (0)35 6037647 3762 CT Soest email : J.Warmer@klasse.nl The Netherlands internet: http://www.klasse.nl


Date view Thread view Subject view Author view