Eclipse Community Forums: EMF "Technology" (Ecore Tools, EMFatic, etc) » Equality operation contract in OCL expressions?

Help

Home

Home » Modeling » EMF "Technology" (Ecore Tools, EMFatic, etc) » Equality operation contract in OCL expressions?

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

Equality operation contract in OCL expressions? [message #30717]

Mon, 10 April 2006 19:20

Radomil Dvorak

Messages: 249
Registered: July 2009

Senior Member

Hi,

I can see that semantics of the '=' operation has changed in EMFT OCL
1.0.0M6.
The difference is in applying '=' operation when the source or the argument
is 'null' /* OclVoid 'null' instance in OCL2.0 */.

Consider the following expression in the context of ecore::EClass instance
with the 'name' attribute set to 'null' value.
context ecore::EClass inv: 'value' = self.name

Currently, this expression results in OclInvalid while the implementation
prior to M6 returned false.
Actually, I think that according to the older OCL spec it was wrong (but
practical ;-)) as the spec (see A.2.2) is fairly strict about the equality
contract requiring all parts be defined.

However, I'm a bit in doubts about the latest OCL2.0 compliant
implementation.
The latest OCL2.0 spec says that any property call applied on the 'null'
instance of OclVoid results in OclInvalid.
I'm not sure that this is explanatory enough to justify the expression above
evaluated to OclInvalid,
because the '=' operation was performed on a valid String object only taking
the valid 'null' value as an argument.

I believe this should not result in OclInvalid, AFAIU, the concept of
'absent value' based on OclVoid was
introduced to enable passing 'null' values to collection operations as
collections now can contain 'null' values.
Is not this analogical situation?

Moreover, when looking at some pre:, post: conditions for several
operations defined in the latest OCL2.0 spec, it looks like
the equality operation on 'null' values should allways result in a boolean
value.
For instance,

Sequence::append (object: T) : Sequence(T)
post: result->size() = self->size() + 1
post: result->at(result->size() ) = object
post: Sequence{1..self->size() }->forAll(index : Integer |
result->at(index) = self ->at(index))

In my opinion, the second post condition could never hold true in case the
'null' value is added and we are not able to produce boolean value from
'null = null'.
Perhaps, I have missed something in the specification and this case is
correct.
If it is this way, I find it quite impractical when writing expressions
which must check for 'null' values explicitly. ;-(

Regards,
/Radek

Report message to a moderator

Re: Equality operation contract in OCL expressions? [message #30786 is a reply to message #30717]

Mon, 10 April 2006 22:27

Eclipse User

Originally posted by: cdamus.ca.ibm.com

Hi, Radek,

The Invalid and OclVoid types both define "=" and "<>" operations, so these
should never return OclInvalid.

I am also a little perplexed as to why 'value' = self.name should have
apparently turned the evaluation around to produce OclInvalid.

This is definitely a bug in the implementation. Care to raise a bugzilla
(sounds like a serious problem)?

Thanks,

Christian

Radek Dvorak wrote:

> Hi,
>
> I can see that semantics of the '=' operation has changed in EMFT OCL
> 1.0.0M6.
> The difference is in applying '=' operation when the source or the
> argument is 'null' /* OclVoid 'null' instance in OCL2.0 */.
>
> Consider the following expression in the context of ecore::EClass instance
> with the 'name' attribute set to 'null' value.
> context ecore::EClass inv: 'value' = self.name
>
> Currently, this expression results in OclInvalid while the implementation
> prior to M6 returned false.
> Actually, I think that according to the older OCL spec it was wrong (but
> practical ;-)) as the spec (see A.2.2) is fairly strict about the equality
> contract requiring all parts be defined.
>
> However, I'm a bit in doubts about the latest OCL2.0 compliant
> implementation.
> The latest OCL2.0 spec says that any property call applied on the 'null'
> instance of OclVoid results in OclInvalid.
> I'm not sure that this is explanatory enough to justify the expression
> above evaluated to OclInvalid,
> because the '=' operation was performed on a valid String object only
> taking the valid 'null' value as an argument.
>
> I believe this should not result in OclInvalid, AFAIU, the concept of
> 'absent value' based on OclVoid was
> introduced to enable passing 'null' values to collection operations as
> collections now can contain 'null' values.
> Is not this analogical situation?
>
> Moreover, when looking at some pre:, post: conditions for several
> operations defined in the latest OCL2.0 spec, it looks like
> the equality operation on 'null' values should allways result in a boolean
> value.
> For instance,
>
> Sequence::append (object: T) : Sequence(T)
> post: result->size() = self->size() + 1
> post: result->at(result->size() ) = object
> post: Sequence{1..self->size() }->forAll(index : Integer |
> result->at(index) = self ->at(index))
>
> In my opinion, the second post condition could never hold true in case the
> 'null' value is added and we are not able to produce boolean value from
> 'null = null'.
> Perhaps, I have missed something in the specification and this case is
> correct.
> If it is this way, I find it quite impractical when writing expressions
> which must check for 'null' values explicitly. ;-(
>
> Regards,
> /Radek

Report message to a moderator

Re: Equality operation contract in OCL expressions? [message #30856 is a reply to message #30786]

Tue, 11 April 2006 08:16

Radomil Dvorak

Messages: 249
Registered: July 2009

Senior Member

Raised request https://bugs.eclipse.org/bugs/show_bug.cgi?id=136068

"Christian W. Damus" <cdamus@ca.ibm.com> wrote in message
news:e1em42$q5p$1@utils.eclipse.org...
> Hi, Radek,
>
> The Invalid and OclVoid types both define "=" and "<>" operations, so
> these
> should never return OclInvalid.
>
> I am also a little perplexed as to why 'value' = self.name should have
> apparently turned the evaluation around to produce OclInvalid.
>
> This is definitely a bug in the implementation. Care to raise a bugzilla
> (sounds like a serious problem)?
>
> Thanks,
>
> Christian
>
>
> Radek Dvorak wrote:
>
>> Hi,
>>
>> I can see that semantics of the '=' operation has changed in EMFT OCL
>> 1.0.0M6.
>> The difference is in applying '=' operation when the source or the
>> argument is 'null' /* OclVoid 'null' instance in OCL2.0 */.
>>
>> Consider the following expression in the context of ecore::EClass
>> instance
>> with the 'name' attribute set to 'null' value.
>> context ecore::EClass inv: 'value' = self.name
>>
>> Currently, this expression results in OclInvalid while the implementation
>> prior to M6 returned false.
>> Actually, I think that according to the older OCL spec it was wrong (but
>> practical ;-)) as the spec (see A.2.2) is fairly strict about the
>> equality
>> contract requiring all parts be defined.
>>
>> However, I'm a bit in doubts about the latest OCL2.0 compliant
>> implementation.
>> The latest OCL2.0 spec says that any property call applied on the 'null'
>> instance of OclVoid results in OclInvalid.
>> I'm not sure that this is explanatory enough to justify the expression
>> above evaluated to OclInvalid,
>> because the '=' operation was performed on a valid String object only
>> taking the valid 'null' value as an argument.
>>
>> I believe this should not result in OclInvalid, AFAIU, the concept of
>> 'absent value' based on OclVoid was
>> introduced to enable passing 'null' values to collection operations as
>> collections now can contain 'null' values.
>> Is not this analogical situation?
>>
>> Moreover, when looking at some pre:, post: conditions for several
>> operations defined in the latest OCL2.0 spec, it looks like
>> the equality operation on 'null' values should allways result in a
>> boolean
>> value.
>> For instance,
>>
>> Sequence::append (object: T) : Sequence(T)
>> post: result->size() = self->size() + 1
>> post: result->at(result->size() ) = object
>> post: Sequence{1..self->size() }->forAll(index : Integer |
>> result->at(index) = self ->at(index))
>>
>> In my opinion, the second post condition could never hold true in case
>> the
>> 'null' value is added and we are not able to produce boolean value from
>> 'null = null'.
>> Perhaps, I have missed something in the specification and this case is
>> correct.
>> If it is this way, I find it quite impractical when writing expressions
>> which must check for 'null' values explicitly. ;-(
>>
>> Regards,
>> /Radek
>

Report message to a moderator