Re: OCL constraints on mutator methods



Date view Thread view Subject view Author view

Richard Mitchell (richard@inferdata.com)
Fri, 12 Apr 2002 14:09:41 +0100


Hi, I want to add a note on the UML v. Eiffel levels of thinking about stacks, rather than on the issue of Larch v. OCL styles. ----- Original Message ----- From: "Shane Sendall" <Shane.Sendall@epfl.ch> To: <puml-list@cs.york.ac.uk> Sent: Tuesday, April 09, 2002 10:02 AM Subject: Re: OCL constraints on mutator methods > 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 An association between Stack and Element at the UML modeling level translates directly to an Eiffel query to return a list-like structure containing a stack's current elements, in order. The purpose of this query is to provide (most of) a conceptual model of stacks. The contracts on methods such as push and pop can then specify the effects of these mutators on this query (and other queries, such as count). Of course, the 'elements' query does not expose the underlying data structure used to actually hold a stack's elements, but can be calculated from that data structure. If you change the data structure, you'll rewrite the calculation of the 'elements' query, too. Further, the 'elements' query does not tell you any secrets about a stack: you can always find out every element on a stack using its 'pop' method to run right the way down the stack. It's kinda reassuring when the conceptual model of stacks (or queues or customer-manager-components or ...) is the same at both the UML and Eiffel (or Java or ...) levels. Best wishes, -- Richard -- -- -- -- -- -- -- Dr. Richard Mitchell Senior Consultant InferData Corp. www.inferdata.com > 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". > > > > > > > > > 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