[pivot] CollectionLiterals have inadequate bounds.

[eclipse-ocl-bot]

| --- | --- | | Bugzilla Link | 540244 | | Status | NEW | | Importance | P3 normal | | Reported | Oct 18, 2018 05:23 EDT | | Modified | Aug 09, 2021 05:50 EDT | | See also | 520440 | | Reporter | Ed Willink |

Description

The following reports a warning that The 'Property::CompatibleDefaultExpression' constraint is violated for 'p::c::ports'

package p : p = 'p'\ {\ class c\ {\ property endpoints : Port[*|1] { ordered };\ property ports : Port[2|1] { ordered } {\ initial: let v = OrderedSet(Port[2|1]){endpoints->first(), endpoints->last()} in v;\ }\ }\ class Port;\ }

Hovering over the "v" reveals

LetVariable v : OrderedSet(p::Port[*|1])[1] = OrderedSet{endpoints->first(), endpoints->last()}

strongly suggesting that the upperbound of the literal is * rather than 2.

While not all bounds can be computed, this one clearly can.

(Also the validation message is far from helpful, and it would be nice to hover somewhere to determine the type of the OrderedSet without introducing a let. Also specifying explicit OrderedSet multiplicity makes no difference.)

[eclipse-ocl-bot]

By Ed Willink on Oct 18, 2018 05:50

(In reply to Ed Willink from comment #0)

While not all bounds can be computed, this one clearly can.

Oh no it can't. It requires too much symbolic analysis to prove that endpoints->first() and endpoints->last() are not the same. If they are the same the OrderedSet Literal is actually of dimension [1..1]. The CollectionLiteralExp safe approach of always reverting 'hard' analyses to the legacy [0..*] is not wrong.

The real question is therefore whether there is a way for users to indicate that they know 'better'. Introducing an @suppressWarnings ... is daunting. In this case surely

initial: let v = OrderedSet{endpoints->first(), endpoints->last()}->oclAsType(OrderedSet(Port[2|1])) in v;

should work? Hovering over the "v" it does. We just need to fix the overenthusiastic assignment/initializer check and message.

[eclipse-ocl-bot]

By Ed Willink on Oct 18, 2018 06:02

The cast does work; I was being fooled by a bad editor refresh - different problem. Solution add the explicit cast:

initial: OrderedSet{endpoints->first(), endpoints->last()}->oclAsType(OrderedSet(Port[2|1]));

This will actually incur a run-time cost as the user's assertion is validated.

---

Bug remains open to resolve:

• poor quality of "The 'Property::CompatibleDefaultExpression' constraint is violated for 'p::c::ports'" diagnostic

• inadequate hovertext for CollectionLiteralExps - the specialized type is actually shown on the "{". It could be available on the "," and "}" too.

[eclipse-ocl-bot]

By Christopher Gerking on Oct 18, 2018 07:58

(In reply to Ed Willink from comment #2)

The cast does work;

Right, thanks a lot.

(In reply to Ed Willink from comment #1)

If they are the same the OrderedSet Literal is actually of dimension [1..1].

Just out of curiosity, would Sequence or Bag allow to detect this dimension more precisely because they don't drop duplicates?

[eclipse-ocl-bot]

By Ed Willink on Oct 18, 2018 08:28

(In reply to Christopher Gerking from comment #3)

(In reply to Ed Willink from comment #1)

If they are the same the OrderedSet Literal is actually of dimension [1..1]. Just out of curiosity, would Sequence or Bag allow to detect this dimension more precisely because they don't drop duplicates?

Yes Bag and Sequence literals could be accurate multiplicity-wise. Overall there are probably quite a few cases that could be handled particularly if operations have per-operation static multiplicity analysis rules. Of course this all goes beyond 'OCL' where non 1/* multiplicity does not exist at all.

[eclipse-ocl-bot]

By Ed Willink on Aug 08, 2021 13:02

(In reply to Ed Willink from comment #1)

It requires too much symbolic analysis to prove that

The Bug 520440 work introduces extra symbolic analysis that detects that the first() and last() are unsound on a [*|1] endpoints.

first() and last() can only be sound if the endpoints declaration which was omitted from the original email is declared or proven to be at least 1, preferably 2. There is no foundation for a proof so the endpoints declaration must be OrderedSet(Port[2..*|1]) so that ports can be OrderedSet(Port[2|1]).

[eclipse-ocl-bot]

By Ed Willink on Aug 09, 2021 05:50

Works fine with symbolic analysis as:

property endpoints : OrderedSet(Port[2|1]);\
property ports : OrderedSet(Port[2|1]) {\
  initial: let v = OrderedSet{endpoints->first(), endpoints->last()}\
    ->oclAsType(OrderedSet(Port[2|1])) in v; }

Fundamentally the OCL for a derived property has only two choices for garbage-in:

a) the new symbolic analysis detects the garbage-in as a compile-time error\ b) the user OCL provides an 'ErrorPort' that is used as 'ok' garbage-out