Re: A question on OCL



Re: A question on OCL

From: Daniel Jackson <dnj_at_mit.edu>
Date: Thu, 18 Dec 2008 17:50:15 -0500
Message-Id: <E36BED63-A6B2-4988-911E-7180D96756D9@mit.edu>
Robert,

Yes, you're exactly right. If you want to make it explicit, which may  
be wise, you can do this:

> sig Library {
> 	items: set Item,
> 	borrowers: set Person
> 	}
> 	{
> 	items in  Journal + Proceeding implies borrowers in Faculty
> 	}
>
> sig Item {}
> sig Journal, Proceeding extends Item {}
>
> sig Person {}
> sig Faculty extends Person {}

The fact inside the Library sig has its fields implicitly qualified;  
it's like a context in OCL. You can make this explicit too:

> fact {
> 	all l: Library | l.items in  Journal + Proceeding implies  
> l.borrowers in Faculty
> 	}


The nice thing about making this context explicit is that we can now  
name the different contexts. For example, we can introduce the set of  
AcademicLibraries whose borrowers are faculty and whose items are  
journals and proceedings:

> sig Library {
> 	items: set Item,
> 	borrowers: set Person
> 	}
>
> sig AcademicLibrary extends Library { }
> 	{
> 	items in  Journal + Proceeding
> 	borrowers in Faculty
> 	}

Now if I can pose questions such as

> // is a library with only journals and proceedings necessarily an  
> AcademicLibrary?
> check {
> 	all l: Library | l.items in Journal + Proceeding implies l in  
> AcademicLibrary
> 	}


and if you run this, you get the expected counterexample.

Daniel



On Dec 18, 2008, at 4:24 PM, Robert France wrote:

> Daniel,
> I see your point.  Correct me if I'm wrong, but from the Alloy  
> specification there seems
> to be a notion of a 'system' consisting of finite sets of Journal,  
> Proceeding and Faculty. The relationship on which
> the fact is based is that the elements referenced are part of this  
> 'system' (note I am not saying there is an association between  
> Faculty and Item). To do the same in OCL it seems you can use an  
> explicit `system' context
> (introduce a somewhat artificial 'system' class with a "part-of"  
> relationship to all other classes in the model) or use the  
> allInstances to get around context issue as Earl suggests (do we  
> really get around the context issue this way?).
> Then again there may be a fix in OCL 2.0 that I'm not aware of.  
> Hopefully some of the OCL 2.0 folks are still
> on this list.
>
> Robert
>
> Daniel Jackson wrote:
>> 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
>>
>
> -- 
> Robert B. France, Professor       | Tel: 970-491-6356
> Computer Science Department       | Fax: 970-491-2466
> Colorado State University         | Email: france@cs.colostate.edu
> Fort Collins, CO 80523            | www.cs.colostate.edu/~france/
>
>
>
>
> To remove yourself from this list please mail puml-list- 
> request@cs.york.ac.uk
> with a message containing the word "unsubscribe".
>
Received on Thu 18 Dec 2008 - 22:50:10 GMT