Re: OCL constraints on mutator methods



Date view Thread view Subject view Author view

Tony Simons (a.simons@dcs.shef.ac.uk)
Wed, 17 Apr 2002 09:14:53 +0100 (BST)

  • Next message: GERARD Sebastien 166342: "Summer school in France on "Model-oriented Technologies for Embed ded Systems Development""

    Thanks to all who have sent interesting replies. Both Shane Sendall and Richard Mitchell have advanced the idea that a Stack could have an association with its Element type and try to create assertions that use OCL's generic collection methods. In this case, we are writing axioms over a sequence, or possibly a bag, of elements instead. I grant that this would work; however, from my point of view, I don't want to have to rely on *any* behaviour that is not part of the abstract specification of the datatype concerned. Having an elements() method that returns a sequence of Elements from a Stack is rather like deferring the specification problem to another type, reminiscent eg of Z's way of basing a Stack on a Sequence, and a Sequence on a Map from ints to values. It is tantamount to relying on the properties of some other type, which is used as the implementation of the Stack. (Though this is less obvious, since a Sequence is an abstraction that generalises over the concrete List or Vector normally used for a Stack). My ulterior motive is to be able to construct minimal specifications, from which minimal test-sets can be generated. The problem with adding "service methods" that reveal a representation with more algebraic structure is that you have to construct many more axioms to prove the correctness of the interrelationship between these extra methods and the salient methods that form the usual interface of the datatype. Also, you then have to prove the correctness of a Sequence. This significantly increases both the specification and the testing obligations, which I am anxious to avoid. Best wishes, --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