Re: OCL foundation



Re: OCL foundation

From: Steffen Zschaler ^lt;sz9@inf.tu-dresden.de>
Date: Fri 10 Mar 2006 - 16:55:27 GMT
Message-ID: <4411AF7F.9010001@inf.tu-dresden.de>
Hi,

As far as I know, the formal (in your sense) foundation used to be in 
Mark Richter's PhD thesis. This used to be the semantics chapter of a 
pre-final version of the submission, but was then moved to the 
non-normative appendix in favour of the MMF-based approach that is now 
in the standard. During revisions it seems to have disappeared magically...

Best,

Steffen

GERARD Sebastien 166342 wrote:
> Hi all,
>
> about the formal defintion of OCL. Is anybody abble to say me what is the formal (in the sens of mathematical) foundation of OCL2?
>
> Thanks,
> regards,
> sébastien
>
> -----------------------------------------
> Sébastien Gérard
> PhD - Ing.
> Head of the Accord-UML research project
> DRT-List/DTSI/SOL/LLSP - CEA/Saclay
> F-91191 Gif sur Yvette Cedex - France
> sebastien DOT gerard AT cea DOT fr
> Phone/fax : +33 1 69 08 58 24 / 83 95
>  
>
>   
>> -----Message d'origine-----
>> De : puml-list-request@cs.york.ac.uk 
>> [mailto:puml-list-request@cs.york.ac.uk] De la part de Prof. 
>> Dr. Peter H. Schmitt
>> Envoyé : vendredi 10 mars 2006 16:03
>> À : puml-list@cs.york.ac.uk; D H. Akehurst; Steffen Zschaler; 
>> Thomas Baar
>> Objet : Re: Automatic conversion
>>
>> My understanding is more or less what you explain below.
>> My question is: where is this mentioned in the OCL Standard?
>> (I am using the version from June 2005).
>> Especially, that undefined is converted to empty set I had 
>> not seen before. Is this a tool builder's interpretation to 
>> make up for an underspecification in the Standard or is it there?
>>
>>
>> regards
>>
>> Peter
>>
>> D H. Akehurst wrote:
>>     
>>> The difference between dot and arrow:
>>>
>>> '->' is an operator that indicates an operation on a 
>>>       
>> collection object, and will convert a non collection to a 
>> collection if necessary.
>>     
>>> '.' is an operator on non collection objects. If applied to 
>>>       
>> a collection it is interpreted as '->collect(x|...)' operation.
>>     
>>> Let us take the following example
>>>
>>> class Person {
>>>   name : String
>>> }
>>>
>>> class AddressBook {
>>>   people : Set(Person)
>>> }
>>>
>>> If we have the following objects (please excuse the notaion used to 
>>> define the variables)
>>>
>>>  p:Person = Person{name='Fred'}
>>>  p2:Person = Person{name='Jane'}
>>>  pu:Person = undefined
>>>  bk:AddressBook = AddressBook{ people=Set{p,p2} }
>>>
>>> then
>>>
>>> p.name : String = 'Fred'
>>> p->collect(x|x.name) = Set{p}->collect(x|x.name) = Bag{'Fred'}
>>> bk->collect(x|x.name) = Bag{'Fred','Jane'}
>>> bk.name = bk->collect(x|x.name) = Bag{'Fred','Jane'}
>>>
>>> p->forAll(x|x='Fred'):Boolean = true
>>> pu.name:String = undefined
>>> Set{undefined} = Set{}
>>> Set{pu} = Set{}
>>> pu->collect(x|x.name) = Set{pu}->collect(x|x.name) = 
>>> pu->Set{undefined}->collect(x|x.name) = Set{}->collect(x|x.name) = 
>>> pu->Bag{} forAll(x|x='Fred'):Boolean = 
>>>       
>> Set{pu}->forAll(x|x='Fred') = 
>>     
>>> pu->Set{}->forAll(x|x='Fred') = true
>>> p->isEmpty() = Set{p}->isEmpty() = false
>>> pu->isEmpty() = Set{pu}->isEmpty() = Set{}->isEmpty() = true
>>>
>>> this all seems pretty consistent to me. You just have to 
>>>       
>> accept that the undefined value equates to an empty set when 
>> collection operations are applied to it (I don't know if this 
>> make sense from a formal/mathemetical perspective). And 
>> understand that an undefined value does not exist inside a 
>> collection; i.e. you cannot have a collection with an 
>> undefined value in it.
>>     
>>> Set{undefined,p} = Set{p}
>>>
>>> Hence,
>>>   self.person->forAll(... 
>>> is the same as
>>>   Set{self.person}->forAll(...
>>>
>>> and
>>>   _emptyset_ -> forAll(...)
>>> is the same as
>>>   Set{_oclVoid_}->forAll(..)
>>> because
>>>   Set{_oclVoid_} = _emptyset_
>>>
>>> (I am assuming that by Set{_oclVoid_} you mean a Set containing an 
>>> undefined value)
>>>
>>>       
>>>> -----Original Message-----
>>>> From: puml-list-request@cs.york.ac.uk 
>>>> [mailto:puml-list-request@cs.york.ac.uk] On Behalf Of Thomas Baar
>>>> Sent: 10 March 2006 13:34
>>>> To: puml-list@cs.york.ac.uk
>>>> Subject: Automatic conversion
>>>>
>>>> D H. Akehurst wrote:
>>>>
>>>>         
>>>>> You can use the invariant
>>>>>
>>>>> context Department inv: 
>>>>>  self.person->forAll(salary < self.maxSalaryDept)
>>>>>
>>>>> In the case where the multiplicity is [0..1].
>>>>>
>>>>> Using the '->' operator on objects that are not collections
>>>>>           
>>>> automatically wraps
>>>>         
>>>>> the object in a Set.
>>>>>
>>>>> Wraping an undefined value into a set results in an empty
>>>>>           
>>>> set, hence your expression
>>>>         
>>>>> gives true when there are no managers.
>>>>>
>>>>>
>>>>>           
>>>> Dave,
>>>>
>>>> I'm very puzzled by the automatic conversion to 
>>>>         
>> collections, it would 
>>     
>>>> mean that, for example,  5->forAll(x| ...) would be syntactically 
>>>> correct!
>>>> What would then be the point to have two different 
>>>>         
>> operators '.' (dot) 
>>     
>>>> and '->' (arrow) in OCL? So far, it helped the reader to 
>>>>         
>> find out if 
>>     
>>>> the source expression is of object or collection type.
>>>>
>>>>
>>>> Another question about the emptySet <-> undefined conversion: 
>>>> Wouldn't it be
>>>> wise to have the following two constraints equivalent (in case of 
>>>> multiplicity [0..1]?
>>>>
>>>>
>>>>
>>>> context Department inv: 
>>>>   self.person->forAll(...   -- here the object self.person 
>>>> is automatically converted into a collection
>>>>
>>>>
>>>> context Department inv: 
>>>>   Set{self.person}->forAll(...   -- here the object 
>>>> self.person is manually converted into a collection
>>>>                                  -- by wrapping it with Set{  }
>>>>
>>>>
>>>>
>>>> Both versions are however not equivalent once that automatic 
>>>> emptySet<-> 
>>>> undefinedness
>>>> conversion is adopted. If self is not linked with any other 
>>>> person then 
>>>> in case
>>>> of automatic conversion we had
>>>>
>>>> context Department inv: _emptyset_ -> forAll(...) 
>>>> what evaluates always to true.
>>>>
>>>> In case of manual conversion we had
>>>>
>>>> context Department inv: Set{_oclVoid_}->forAll(..)
>>>> what is not always true.
>>>>
>>>> To summary: The automatic conversion of x into a collection 
>>>> type cannot 
>>>> be simulated by
>>>> Set{x}. However, this would be (at least for me) the most natural 
>>>> semantics for the automatic conversion...
>>>>
>>>> Best regards,
>>>> Thomas
>>>>
>>>>
>>>> -- 
>>>> Dr. Thomas Baar
>>>> Software Engineering Laboratory
>>>> School of Computer and Communication Sciences EPFL
>>>> EPFL IC UP-LGL
>>>> INJ 337 (Bâtiment INJ)
>>>> Station 14
>>>> CH-1015 Lausanne, Switzerland
>>>> Tel +41 21 693 2580, Fax +41 21 693 5079
>>>> mailto:thomas.baar@epfl.ch   http://lgl.epfl.ch/members/baar/
>>>> ********************************************************
>>>> Do not miss MoDELS/UML 2006: see 
>>>> http://www.modelsconference.org for the 9th International 
>>>> Conference on Model Driven Engineering Languages and Systems 
>>>> (formerly the UML series of conferences)
>>>>
>>>>
>>>>
>>>>
>>>>
>>>>
>>>>
>>>> To remove yourself from this list please mail 
>>>> puml-list-request@cs.york.ac.uk
>>>> with a message containing the word "unsubscribe".
>>>>
>>>>
>>>>         
>>>
>>> To remove yourself from this list please mail 
>>>       
>> puml-list-request@cs.york.ac.uk
>>     
>>> with a message containing the word "unsubscribe".
>>>
>>>
>>>       
>> -- 
>> Prof.Dr.P.H.Schmitt
>> Fakultät für Informatik
>> Universität Karlsruhe
>>
>>
>>
>> To remove yourself from this list please mail 
>> puml-list-request@cs.york.ac.uk
>> with a message containing the word "unsubscribe".
>>
>>
>>     

-- 
Dipl.-Inf. Steffen Zschaler
Research Assistant

Technische Universität Dresden
Department of Computer Science

Phone +49 351 463 38555
Fax   +49 351 463 38459
Email Steffen.Zschaler@tu-dresden.de
WWW   http://www.steffen-zschaler.de.vu/
Received on Fri Mar 10 16:57:37 2006