Re: allInstances at pre

Re: allInstances at pre

From: Andreas Awenius ^lt;>
Date: Tue 10 May 2005 - 19:35:18 BST
Message-ID: <C2r8Aj4oY3yUs27zgLTbQsPINMe8nMJEhXAZNVEXibu@akmail>
Hello all,

> I still owe you an answer to one of your questions:

> Andreas Awenius wrote:
>>>This is okay except for the fact the OCL does not allow you
>>>to attach @pre to allInstances.
>> Why do you think this?

> What makes me think so?
> The standard document "UML 2.0 OCL Specification" ptc/03-10-14
> which I believe is the latest word in the OCL 2.0 standard.

> On page 79 the grammar rules for OperationCallExpCS are given.
> These are the only rules where @pre is dealt with. Since
> allInstances is a class operation part [G] applies. But, as you see,
> no @pre allowed here.
> Also the construct "User@pre" in your proposed solution  is not covered
> by the standard grammar. "User" maps to the non-terminal "pathNameCS"
> and as can be seen, again from production [G], no @pre allowed here.

allInstances() is not a class operation, it is an instance operation of class OclAny.
The expression User@pre.allInstances() is variation E of OperationCallExpCS.

Let me cite from the specification:

11.2.4 Operations and well-formedness rules

allInstances() : Set( T )
Returns all instances of self. Type T is equal to self. May only be used for classifiers that have a finite number of
instances. This is the case for, for instance, user defined classes because instances need to be created explicitly. This is not the case for, for instance, the standard String, Integer, and Real types.
pre: self.isKindOf( Classifier ) -- self must be a Classifier
and -- TBD -- self must have a finite number of instances
-- it depends on the UML 2.0 metamodel how this can be
-- expressed
post: -- TBD

Please note the precondition, that says that the called object must be a Classifier (like 'User' in your example).

Therefore, I still think that our checker is right.

> One could argue that this is simply an error in the standard. Is there
> somebody in the OMG who cares?

> It would be interesting to hear what the other OCL tools do(we have
> recently witnessed a number of announcments of new OLC tools on this
> mailing list). Do they accept @pre for class operations? Do they
> accept @pre an pathNames?

They should not accept @pre on class operations but they should accept it with pathNames if the pathName yields a classifier (for example, if 'User' is defined in package 'A'). But as you have written, this is not permitted by the OCL specification.

For example, with this fragment:

context A::User::addUser(c:Name)
pre: A::User.allInstances()->forAll(u1 | <> c)

post: A::User.allInstances()-> exists( u1 | u1.oclIsNew()
                       and = c
                       A::User.allInstances() =  A::User@pre.allInstances() -> including(u1))

our OCL AddIn for Rational Rose gives this error:

unexpected token: @pre [file: , line: 7, column: 57]

This means, that pathName@pre is already forbidden by the grammar.

I tried to check the code fragment I sent in my earlier message with Octopus 2.0 but got an error message during the XMI import.

Best regards,

> regards

> Peter

> --
> Prof.Dr.P.H.Schmitt
> Fakultät für Informatik
> Universität Karlsruhe

> To remove yourself from this list please mail
> with a message containing the word "unsubscribe".

Andreas Awenius
EmPowerTec AG
Taubenweg 20
85238 Petershausen, Germany
Fon: +49 8137 80 98 81
Fax: +49 8137 80 98 82
Received on Tue May 10 19:33:14 2005