Issue 14980: OCL 2.1 11.7.3 OrderedSet addition well-formedness rules (ocl2-rtf)
Source: Model Driven Solutions (Dr. Edward Willink, ed(at)willink.me.uk)
Nature: Uncategorized Issue
Severity: 
Summary: The OrderedSet well-formedness constraints in 11.7.3 appear to have been
copied and pasted from Sequence. They need revision to consider the Set
consequences of .


Addition operations (includes, insertAt, union, append, prepend) have a
post-condition that the size increases, which is clearly not the case if
an additional element is equal to a pre-existing element.


In the particular case of insertAt there is an ambiguity as to whether
the insert index is the pre or post index. For instance when inserting 3
at index 5 into OrderedSet{1, 2, 3, 4, 5, 6} the pre-index insertion
yields OrderedSet{1,2,4,3,5,6} whereas the post-index insertion yields
OrderedSet{1,2,4,5,3,6}. While the post-index insertion satisfies the
'post: result->at(index) = object' constraint, it is presumably not the
intent.

Resolution: 
Revised Text: 
Actions taken:
January 17, 2010: received issue
Discussion: 

End of Annotations:=====
ronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: ApoEAKKyUkvUnw4R/2dsb2JhbADTWIQyBA
Date: Sun, 17 Jan 2010 14:49:15 +0000
From: Ed Willink <ed@willink.me.uk>
User-Agent: Mozilla/5.0 (Windows; U; Windows NT 6.0; en-GB; rv:1.9.1.5) Gecko/20091204 Thunderbird/3.0
To: issues@omg.org
Subject: OCL 2.1 11.7.3 OrderedSet addition well-formedness rules
X-Plusnet-Relay: bcc658d7d7070695c98d2506d8d7e454


Hi


The OrderedSet well-formedness constraints in 11.7.3 appear to have been
copied and pasted from Sequence. They need revision to consider the Set
consequences of .


Addition operations (includes, insertAt, union, append, prepend) have a
post-condition that the size increases, which is clearly not the case if
an additional element is equal to a pre-existing element.


In the particular case of insertAt there is an ambiguity as to whether
the insert index is the pre or post index. For instance when inserting 3
at index 5 into OrderedSet{1, 2, 3, 4, 5, 6} the pre-index insertion
yields OrderedSet{1,2,4,3,5,6} whereas the post-index insertion yields
OrderedSet{1,2,4,5,3,6}. While the post-index insertion satisfies the
'post: result->at(index) = object' constraint, it is presumably not the
intent.


Regards


Ed Willink