Eclipse Community Forums: OCL » Nested OCL forAlls

Help

Home

Home » Modeling » OCL » Nested OCL forAlls

Show: Today's Messages :: Show Polls :: Message Navigator

Nested OCL forAlls [message #1703513]

Sun, 02 August 2015 00:31

Hamid Qartal

Messages: 33
Registered: December 2013

Member

I have the following Formula in First Order Logic.

    foAll a:A | forAll b :B | if a.r1=b then a.r2=b

simply, for all objects of type A, and for all objects of type B, if they are related by r1 then they are related by r2 as well. r1 and r2 are two association from A to B.

How this is written in OCL?

Report message to a moderator

Re: Nested OCL forAlls [message #1703518 is a reply to message #1703513]

Sun, 02 August 2015 09:13

Ed Willink

Messages: 5834
Registered: July 2009

Senior Member

Hi

A.allInstances()->forAll(a | B.allInstances()->forAll(b | a.r1=b implies
a.r2=b))

---

OCL 2.5 may accept that allInstances() is an unavoidably useful evil and
so allow

forAll(a : A, b : B| a.r1=b implies a.r2=b)

Regards

Ed Willink

On 02/08/2015 01:31, Hamid Qartal wrote:
> I have the following Formula in First Order Logic.
>
> foAll a:A | forAll b :B | if a.r1=b then a.r2=b
>
>
> simply, for all objects of type A, and for all objects of type B, if
> they are related by r1 then they are related by r2 as well. r1 and r2
> are two association from A to B.
>
> How this is written in OCL?
>
>
>

Report message to a moderator

Previous Topic:	What specification to use
Next Topic:	How to query UML models with OCL?

Goto Forum:

-=] Back to Top [=-

[ Syndicate this forum (XML) ] [

]

Current Time: Sun Apr 22 10:40:10 GMT 2018

.:: Contact :: Home ::.