Re: allInstances at pre

Re: allInstances at pre

From: Prof. Dr. Peter H. Schmitt ^lt;>
Date: Thu 12 May 2005 - 09:47:03 BST
Message-ID: <>
Steffen Zschaler wrote:
> Dear all,
> Andreas Awenius wrote:
> <snip />
>> 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?
> Why would you want to express something like this? 

This is dodging the issue. I still think my question is reasonable,
even if only just out of scientific interest. A possible outcome of
this discussion "there are certain postconditions that cannot be 
expressed om OCL" is interesting. Regardless of the fact if you want
to use this condition or not.

In fact, in any
> system that doesn't work strictly sequentially, an assertion like this 
> might not even be correct, because users may be deleted by invocations 
> of deleteUser executing concurrently. 

This addresses another issue. OCL does not offer any built-in support
for concurrent programming. Maybe it should not. Also JML, the closest
rival to OCL, did not address until recently the issues of 
multi-threaded programs. Now there is a first paper on this topic.

To express that a new user was
> created simply use a reference to the new object (for example using a 
> call to User.allInstances()->exists()) and assert that it is oclIsNew().

Maybe you did not follow the thread of discussion from the start. The 
example I initially presented was taken from a specification draft by 
NIST on RBAC (role based access control). The specification was written 
in Z, where there is not problem expressing the statement is question.
I tried to translate this into OCL.
In the context of RBAC a strict control of the registered users is 
mandatory and the effects you mentioned caused by concurrency have to be 
avoided. (which of course can be done by placing locks or otherwise).

> Just my 2c,
> Steffen

Fakultät für Informatik
Universität Karlsruhe
Received on Thu May 12 09:47:13 2005