Re: OCL constraints on mutator methods



Date view Thread view Subject view Author view

Shane Sendall (Shane.Sendall@epfl.ch)
Tue, 09 Apr 2002 11:02:40 +0200


Hello, What I see in the first line (invariant below) seems to be out of the spirit of OCL (more something like I would write in Larch). In OCL, you would use the UML model to build a constraint. In this case, there would probably be an association between stack and element (or it could be a template, in which case you could probably use navigation like with associations?) I don't see a major problem by doing the following: context Stack::pop(): Element pre: self.element->notEmpty () post: let top: Element = self.top()@pre in self.element = self.element@pre->excluding (top) and result = top; I would argue that you don't need to go to the effort that you do in Eiffel to ensure information hiding because associations are more abstract than data structures such as arrays. BTW: the reason why you can not do it in Eiffel is because you don't want to break information hiding by using the implementation data structure (e.g., array), i.e., you do not wait to tell the world which data structure you are using (otherwise they may become dependent on this fact and then there code may break when you decide to change the data structure). If you wanted a truly "abstract" contract then you need to define an abstract system state that deals with concepts rather than implementation classes. This does not stop you from using a UML class diagram, however. E.g. http://lglwww.epfl.ch/research/fondue/case-studies/elevator/single-cabin/acm.htm Likewise, Catalysis offers this possibility Cheers, -- Shane --------------------------------------------------------------------- - Shane Sendall - Swiss Federal Institute of Technology in Lausanne - - email : Shane.Sendall@epfl.ch http://lglwww.epfl.ch/~sendall/ - - phone : ++41 21 693 66 89 fax : ++41 21 693 50 79 - Jos Warmer wrote: > 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 > > > > > To remove yourself from this list please mail > puml-list-request@cs.york.ac.uk > with a message containing the word "unsubscribe". >


Date view Thread view Subject view Author view