Home » Modeling » OCL » A conceptual understanding problem with invariant conditions?
| A conceptual understanding problem with invariant conditions? [message #668367] |
Thu, 05 May 2011 12:55  |
 Bernhard Hoisl
Messages: 26
Registered: March 2011 |
Junior Member |
|
|
Hi guys,
I recently ran into a more conceptual problem when applying some of my OCL constraints with Eclipse's OCL console.
I would like to define two invariants complementing each other. As OMG's OCL spec is telling us "invariants must be true for all instances of that type at any time".
Let me show you a very basic example I quickly created as a showcase:
OCL 1
----------------
context ObjectNode inv:
self.incoming->forAll(i | i.source.oclIsKindOf(ObjectNode))
OCL 2a
----------------
context ObjectNode inv:
self.incoming->forAll(i | i.source.ordering->notEmpty())
OCL 2b
----------------
context ObjectNode inv:
self.incoming->forAll(i | i.source.oclAsType(ObjectNode).ordering->notEmpty())
OK, this example is only for showcasing purpose, but I think you should get the problem I am facing. So I define the first OCL constraint, basically saying that a target ObjectNode - if there are any incoming ObjectFlows - must have ObjectNodes (or subtypes thereof) as its sources. So, I factor out any DecisionNodes etc., for example.
As constraint 1 is defined as invariant it must hold for every instance at all time. So, if we look at OCL 2a, I want to express that the property "ordering" of a source ObjectNode of an incoming ObjectFlow must not be empty. And there is the tricky part: As I know from OCL 1 that all source nodes must be ObjectNodes, can I avoid the typing as shown in OCL 2b? Because, actually I know that there is only one type possible (and that is an ObjectNode) and I know that this type owns the property "ordering".
OCL 2b is just expressing the same constraint as OCL 2a but this time with oclAsType() casting.
Of course, Eclipse's OCL console throws an error when inserting OCL 2a because as far as I know there is no possibility to insert two or more invariants and check them at the same time. Or in other words: you cannot check if two or more invariant conditions are true at the same time for all instances (like it is required from the OCL spec - as far as I understand it).
So, my specific question is: Is this just an implementational problem as you cannot easily solve the issue of checking multiple OCL invariants at the same time? And, therefore, are OCL1 and OCL2a proper OCL-compliant statements (please uncouple this question from any implementation issues)? So, are these two OCL compliant (Argumentation 1)?
Or is OCL2a not valid, per se (Argumentation 2)? My other argumentation would be that of course all OCL invariants must be true for all instances for all times, but this does not solve the specific casting problem given in OCL2a. It is true, that only ObjectNodes can be sources of ObjectNodes (OCL1). But when navigating to the source ObjectNode (i.source) you still not know the type of the node navigating to (could nevertheless be any subtype of an ActivityNode). Therefore, when trying to access the property "ordering" you first have to cast the node as an ObjectNode (OCL2b). Because, for example, any ControlNode would not own this property.
I hope I explained my problem clear enough. Could someone help me here by shedding some light on this issue or share his opinion? Somehow I got confused and I don't want to limit the question to implementation issues, but rather want to clarify it conceptually and according to the specs.
Many thanks,
Bernhard
[Updated on: Thu, 05 May 2011 12:59] Report message to a moderator |
|
|
| Re: A conceptual understanding problem with invariant conditions? [message #668371 is a reply to message #668367] |
Thu, 05 May 2011 13:20  |
Ed Willink
Messages: 7655
Registered: July 2009 |
Senior Member |
|
|
Hi Bernhard
Each OCL expression must be syntactically and semantically valid, so
OCL2a is not allowed. (No different to Java; a cast in one place doesn't
obviate a cast elsewhere).
A smart execution envirionment might recognize that OCL2b shares a
prefix execution with OCL1 and so optimize the joint execution. Eclipse
OCL doesn't currently do this.
Regards
Ed Willink
On 05/05/2011 13:55, Bernhard Hoisl wrote:
> Hi guys,
>
> I recently ran into a more conceptual problem when applying some of my
> OCL constraints with Eclipse's OCL console.
>
> I would like to define two invariants complementing each other. As
> OMG's OCL spec is telling us "invariants must be true for all
> instances of that type at any time".
>
> Let me show you a very basic example I quickly created as a showcase:
>
> OCL 1
> ----------------
> context ObjectNode inv:
> self.incoming->forAll(i | i.source.oclIsKindOf(ObjectNode))
>
> OCL 2a
> ----------------
> context ObjectNode inv:
> self.incoming->forAll(i | i.source.ordering->notEmpty())
>
> OCL 2b
> ----------------
> context ObjectNode inv:
> self.incoming->forAll(i |
> i.source.oclAsType(ObjectNode).ordering->notEmpty())
>
>
> OK, this example is only for showcasing purpose, but I think you
> should get the problem I am facing. So I define the first OCL
> constraint, basically saying that a target ObjectNode - if there are
> any incoming ObjectFlows - must have ObjectNodes (or subtypes thereof)
> as its source. So, I factor out any DecisionNodes etc., for example.
>
> As constraint 1 is defined as invariant it must hold for every
> instance at all time. So, if we look at OCL 2a, I want to express that
> the property "ordering" of a source ObjectNode of an incoming
> ObjectFlow must not be empty. And there is the tricky part: As I know
> from OCL 1 that all source nodes must be ObjectNodes, can I avoid the
> typing as shown in OCL 2b? Because, actually I know that there is only
> one type possible (and that is an ObjectNode) and I know that this
> type owns the property "ordering".
>
> OCL 2b is just expressing the same constraint as OCL 2a but this time
> with oclAsType() casting.
>
> Of course, Eclipse's OCL console throws an error when inserting OCL 2a
> because as far as I know there is no possibility to insert two or more
> invariants and check them at the same time. Or in other words: you
> cannot check if two or more invariant conditions are true at the same
> time for all instances (like it is required from the OCL spec - as far
> as I understand it).
>
> So, my specific question is: Is this just an implementational problem
> as you cannot easily solve the issue of checking multiple OCL
> invariants at the same time? And, therefore, are OCL1 and OCL2a proper
> OCL-compliant statements (please uncouple this question from any
> implementation issues)? So, are these two OCL compliant (Argumentation
> 1)?
>
> Or is OCL2a not valid, per se (Argumentation 2)? My other
> argumentation would be that of course all OCL invariants must be true
> for all instances for all times, but this does not solve the specific
> casting problem given in OCL2a. It is true, that only ObjectNodes can
> be sources of ObjectNodes (OCL1). But when navigating to the source
> ObjectNode (i.source) you still not know the type of the node
> navigating to (could nevertheless be any subtype of an ActivityNode).
> Therefore, when trying to access the property "ordering" you first
> have to cast the node as an ObjectNode (OCL2b). Because, for example,
> any ControlNode would not own this property.
>
> I hope I explained my problem clear enough. Could someone help me here
> by shedding some light on this issue or share his opinion? Somehow I
> got confused and I don't want to limit the question to implementation
> issues, but rather want to clarify it conceptually and according to
> the specs.
>
> Many thanks,
>
> Bernhard
|
|
|
Goto Forum:
Current Time: Thu Apr 25 17:58:22 GMT 2024
Powered by FUDForum. Page generated in 5.03426 seconds |
] 
Search
Help
Register
Login
Home
