RE: A question on OCL



RE: A question on OCL

From: Waldin, Earl <Earl.Waldin_at_paranor.ch>
Date: Fri, 19 Dec 2008 12:09:51 +0100
Message-ID: <1DE41A26EA92CA4FB831A9449AB0841E5DCB93@srv-par2.paranor.ch>
Jrn
 
The way you state this is a bit fuzzy and I'm not quite sure I follow your example. Part of my problem is the meaning of the identifiers TheWorld and isNotEnough(), and the other is the use of "one". Firing is a whole different issue and isn't necessary to make sense of things at all. Assuming that TheWorld is a property of a Bond (which is consistent with your example and could mean the world that a given Bond lives in), your invariant is equivalent to (see page 155 of the OCL 2.0 formal 06-05-01 spec)
 
   Bond.allInstances()->select(b | b.TheWorld.isNotEnough()) -> size = 1
 
If there are no Bonds, then this will be false. Therefore, any instance of your UML schema that does not have a Bond will not satisfy this constraint.
 
I'll take a stab at describing my understanding. A UML schema, i.e., a collection of classes with properties and associations, defines a (possibly infinite) set of instances of that schema. OCL constraints are defined at the schema level but are evaluated at the instance level. A given schema instance satisfies a constraint if that constraint evaluates to true for that instance. OCL constraints specify the set of valid schema instances in the following sense. A UML model is a UML schema together with a set of constraints. A valid schema instance is an instance that satisfies all the constraints of a model. The model is in some sense modeling "the world" under consideration. 
 
First we need to distinguish between a model as an abstraction of a set of possible worlds and a model as a specification of a set of possible worlds.
 
In the case of abstraction:
We are given a set of possible worlds and want to model them. Looking from the top down, i.e., from the point of view of the model, those schema instances that satisfy the contraints define the set of valid worlds. Looking from the bottom up, i.e., from point of view of the world, the model is an abstraction of the set of all possbile worlds. Our job as a modeller is to ensure that the set of valid schema instances corresponds to the set of possible worlds. Only then do we have a valid abstraction.
 
In the case of specification:
Here we are not given a set of possible worlds but instead are using a model to define the set of possible worlds. In this case the set of possible worlds is by definition the set of valid schema instances. You get to decide if the set of valid instances is what you want.
 
So, judging the correctness of your model depends on what you are trying to do with it.
 
OCL is pretty much like predicate calculus, at least to a first approximation. What you have to watch out for are vacuous forall statements, see http://en.wikipedia.org/wiki/Vacuous_truth. For example, take the statement:
 
  Bond.allInstances()->forAll(b | b.TheWorld.isNotEnough()) 
 
A schema instance that has no Bonds in it will satisfy this constraint and is therefore a valid world. (Here I mean the world being modelled and not Bond's world. Perhaps this isn't the best example if one wants to avoid confusion!). If the given set of possible worlds includes one that has no such Bond, then this is OK and our model is a valid abstraction. If, however, in every given possible world all Bonds can save their world that is not enough then your model is not a correct abstraction because it allows a valid world that is not a possible world. On the other hand, if we want to specify the set of possible worlds then we allow a world that can't be saved. It's your choice.
 
Now consider the statement:
 
  Bond.allInstances->exists(b | b.The World.isNotEnough())
 
A schema instance that has no Bonds will not satisfy this constraint and therefore is not a valid world. Every valid world will have at least one such Bond. This constraint is what we need if we want to specifiy that, in every world, there is at least one Bond that can save his world that is not enough. Whether or not it is a valid abstraction of some reality is another question! Give me a reality (i.e., a set of possible worlds) and I can answer this question.
 
The statement
 
  Bond.allIstances()->one(b | b.TheWorld.isNotEnough())
 
Only a schema instance that has exactly one Bond that can save his world that is not enough will satisfy this constraint. Whether this is too restrictive is up to debate. Looking at history we know that only Pierce Brosnan has actually saved his world that was not enough. We could argue about whether Sean Connery, or any other Bond, would have been up to the task :-)
 
I hope I haven't confused everybody.
 
    -Earl
 

-----Original Message-----
From: puml-list-request@cs.york.ac.uk [mailto:puml-list-request@cs.york.ac.uk] On Behalf Of Jorn Guy Suess
Sent: Thursday, 18 December, 2008 23:59
To: puml-list@cs.york.ac.uk
Subject: RE: A question on OCL



Arnon,

 

There is one other factor you have to be aware of when using allInstances, and Daniel will know that well, because he was the first to pint out that issue. OCL is an instance-based constraint language. A constraint will, technically speaking, only 'fire' if there is an instance. This can be a dangerous bet. Example (non-UML model, just for fun):

 

Context Bond

inv InternationalRelations:

Bond.allInstances->one(TheWorld.isNotEnough())

 

If there is no special agent in your world, then he (or she) cannot save it. As Daniel has pointed out in the past, the absence of a dedicated "System" Singleton whose existence ensured makes world-level constraints unreliable.

 

The answer to a profile is to mandatorily couple it with a model library (see UML standard terms) and then attach your constraint to a "bogus" model element whose only purpose it is to exist and hence make sure your world-constraints trigger. Sorry, but at the current time there is no other fix for this.

 

Jrn Guy S

 

P.S.: Avoid one in your constraints. That operator leads to OCL non-determinism, which is a bad idea for a profile. You do not want a model to sometimes be valid and not at other times. Watch for these things...

 

From: puml-list-request@cs.york.ac.uk [mailto:puml-list-request@cs.york.ac.uk] On Behalf Of Arnon Sturm
Sent: Friday, 19 December 2008 07:58
To: puml-list@cs.york.ac.uk
Subject: RE: A question on OCL

 

Thank you all for the discussion.

 

As Earl suggested I will try to expand my question. The intention of my question is related to profiles (as Jorg guessed).

 

I would like to restrict stereotypes within a profile and specify dependencies among these.

 

The allInstances solution suggested seems a good one. Yet I am not clear, what the context of that invariant is? do we need a context for that kind of constraints? what is the meaning in that case?

 

 

Arnon

 

 


  _____  


From: puml-list-request@cs.york.ac.uk [mailto:puml-list-request@cs.york.ac.uk] On Behalf Of Waldin, Earl
Sent: Thursday, December 18, 2008 8:38 PM
To: puml-list@cs.york.ac.uk
Subject: RE: A question on OCL

Wow, it's amazing to see this much activity on PUML!

 

Perhaps the misunderstanding has to do with (mis)understanding the original statement of the problem. Like Daniel, I see nothing in the problem statement that would indicate any kind of relationship between journals, proceedings and persons: 

 

  For example, in case of a library system we have two "unrelated" classes: item and person. 

 I would like to specify the follwoing constraint: if the items of a particular system are all of type 'journal' or 'proceeding', then all the persons in this system are of type 'faculty'.

 

Reading an author-publication relationship or some other hidden relationship into this is going beyond the problem as stated. My original OCL constraint, although syntactically far less elegant than that in Alloy, says the same thing as Daniel's:

 

  Item.allInstances()->forAll(i | i.oclIsKindOf(Journal) or i.oclIsKindOf(Proceeding)) implies Person.allInstances()->forAll(p | p.oclIsKindOf(Faculty))

 

I introduced the second version with a Library as context because the statement mentions a library system and the above seems to me to be a statement about a library system and not about the relationship between types of publications and persons, although given the brevity of the statement I could be wrong. There is also the question of what the statement intends with "if the items of a particular system".  Just what is this "particular" system? Is it relevent? If so then Arnon can expand his question to include a more precise description of the problem and we can stop speculating.

 

So let's not read too much into this simple example!

 

    -Earl

 

-----Original Message-----
From: puml-list-request@cs.york.ac.uk [mailto:puml-list-request@cs.york.ac.uk] On Behalf Of Daniel Jackson
Sent: Thursday, 18 December, 2008 18:48
To: puml-list@cs.york.ac.uk
Subject: Re: A question on OCL

I have to say that I'm surprised by the responses to this question. 

 

It doesn't seem to me to be a tricky case at all. Introducing an association strikes me as totally wrong: just consider how that association would be designated (if you don't know what a designation is, see, eg, http://mcs.open.ac.uk/mj665/Hoare99a.pdf). 

 

I try to resist always saying "just do it in Alloy", but in this case I do wonder whether the focus on navigations and contexts in OCL creates a problem where there shouldn't be one.

 

In Alloy, you'd model it like this:

 

sig Item {}

sig Journal, Proceeding extends Item {}

 

sig Person {}

sig Faculty extends Person {}

 

fact {

// if the items of a particular system are all of type 'journal' or 'proceeding',

// then all the persons in this system are of type 'faculty'

Item in Journal + Proceeding implies Person in Faculty

}

 

// show me an example

run {}

 

Daniel

 

On Dec 18, 2008, at 3:35 AM, Arnon Sturm wrote:





All,

 

I wonder whether it is possible to specify an OCL constraint on two or more model elements which do not have a navigation path among them.

 

For example, in case of a library system we have two "unrelated" classes: item and person.

I would like to specify the follwoing constraint: if the items of a particular system are all of type 'journal' or 'proceeding', then all the persons in this system are of type 'faculty'.

 

For sure, there is the possibility to define a "mediator" class that will create navigation paths. However, we are interested in specifying the constraint without that "mediator" class.

 

Thanks for your help,

 

Arnon Sturm

 
Received on Fri 19 Dec 2008 - 11:10:00 GMT