Re: allInstances at pre

Re: allInstances at pre

From: Andreas Awenius ^lt;>
Date: Wed 11 May 2005 - 21:34:42 BST
Message-ID: <A75uu174UJvu1z8uQDLkpNXwa3v14sITyfzzogFHSUk@akmail>
Hello all,

> On 05-mai-05, at 22:26, Andreas Awenius wrote:
>> 			     User.allInstances() =  User@pre.allInstances() ->
>> including(u1))
> I think this is syntactically correct, but not what is wanted.
> "User@pre" will designate the classifier User as it was just before
> AddUser, namely exactly the same.
> Thus you could equivalently write:
> User.allInstances() =  User.allInstances() -> including(u1))

Sounds resonable to me.
As the specification says:
"In a postcondition, the expression can refer to values for each property of
an object at two moments in
So I think that it is safe to assume, that @pre can only be applied to
We have added an additional semantic check to our OCL-AddIn for Rational
Now it says:

@pre is applied to identifier 'User' which is not a property.

The new semantic check will be included in the next release 1.7.4 which is
scheduled for end of June.

That leaves the original posters question open:
How can I express, that no instance was destroyed during the execution of an
operation and only one instance was added?

Best regards,

> 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 Wed May 11 21:32:36 2005