Issue 18504: Collection::any() violates precondition if the collection is empty (ocl2-rtf) Source: (, ) Nature: Revision Severity: Significant Summary: Section 11.9.1.4 states that "there must be at least one element fulfilling body, otherwise the result of this IteratorExp is null." And defines source->any(iterator|body) = source->select(iterator | body)->asSequence()->first() However let seq:Sequence<T>=source->select(body)->asSequence() in source->any(body)=seq->at(1) >From section 11.7.5 context Sequence::first() : T post: result = self->at(1) context Sequence::at(i : Integer) : T pre : i >= 1 and i <= self->size() If there is no element fulfilling body, then seq is empty and the precondition of Sequence::at does not hold because 1 > seq->size(). Related to: Issue 18125 [OCL 2.4] Resolution: The 'equivalent' OCL of source->select(iterator | body)->asSequence()->first() returns invalid if no elements are selected, rather than null as the words say. As identified in Issue 18125, null could also be a valid value, so the words are clearly wrong. Revised Text: In 11.9.1.4 any replace If there is more than one element for which body is true, one of them is returned. There must be at least one element fulfilling body, otherwise the result of this IteratorExp is null. by Returns invalid if any body evaluates to invalid for any element, otherwise if there are one or more elements for which body is true, an indeterminate choice of one of them is returned, otherwise the result is invalid Actions taken: February 26, 2013: received issue December 23, 2013: closed issue Discussion: End of Annotations:===== m: webmaster@omg.org Date: 26 Feb 2013 10:41:43 -0500 To: Subject: Issue/Bug Report ******************************************************************************* Name: Roberto Javier Godoy Employer: Universidad Nacional del Litoral mailFrom: rjgodoy@fich.unl.edu.ar Terms_Agreement: I agree Specification: OCL Section: 11.9.1.4 FormalNumber: formal/2012-01-01 Version: 2.3.1 Doc_Year: 2012 Doc_Month: January Doc_Day: 02 Page: 169 Title: Collection::any() violates precondition if the collection is empty Nature: Revision Severity: Significant CODE: 3TMw8 B1: Report Issue Description: Section 11.9.1.4 states that "there must be at least one element fulfilling body, otherwise the result of this IteratorExp is null." And defines source->any(iterator|body) = source->select(iterator | body)->asSequence()->first() However let seq:Sequence=source->select(body)->asSequence() in source->any(body)=seq->at(1) >From section 11.7.5 context Sequence::first() : T post: result = self->at(1) context Sequence::at(i : Integer) : T pre : i >= 1 and i <= self->size() If there is no element fulfilling body, then seq is empty and the precondition of Sequence::at does not hold because 1 > seq->size(). Related to: Issue 18125 [OCL 2.4] X-CM-Score: 0.00 X-CNFS-Analysis: v=2.0 cv=J7R0GnbS c=1 sm=1 a=eW53zEZrsyElcQ0NK1QpqA==:17 a=_WFI8pCH4AAA:10 a=J240YndNYqYA:10 a=IkcTkHD0fZMA:10 a=YYzpnO7rAAAA:8 a=6gIXP91biRgA:10 a=KHpXyVWLAAAA:8 a=oCcaPWc0AAAA:8 a=q-hY-bVrfbHgantMQh4A:9 a=QEXdDO2ut3YA:10 a=_W_S_7VecoQA:10 a=-zspGdomsggA:10 a=gFGq0ozTCKgA:10 a=c9tJgGcuwpQA:10 a=WP4_USCxRkkA:10 a=U_FOK-r5ADStQRTP:21 a=eW53zEZrsyElcQ0NK1QpqA==:117 Date: Tue, 26 Feb 2013 16:35:46 +0000 From: Ed Willink User-Agent: Mozilla/5.0 (Windows NT 6.0; rv:17.0) Gecko/20130215 Thunderbird/17.0.3 To: ocl2-rtf@omg.org, rjgodoy@fich.unl.edu.ar CC: Juergen Boldt Subject: Re: issue 18504 -- OCL 2 RTF issue X-Virus-Scanned: amavisd-new at omg.org Hi Roberto Thank you for pointing this out; your explanation is difficult to follow, but the 'equivalent' OCL of source->select(iterator | body)->asSequence()->first() returns invalid if no elements are selected, rather than null as the words say. I was already aware that the words were bad because it should be possible for any(x) to return null as the successfully selected value. Therefore the equivalent OCL is correct and the words need changing to "otherwise the result of this IteratorExp is invalid." Perhaps the equivalent OCL should really be source->asSet()->select(iterator | body)->asSequence()->first() to stress the indeterminacy of the choice for an ordered source.  Regards   Ed Willink On 26/02/2013 15:58, Juergen Boldt wrote: From: webmaster@omg.org Date: 26 Feb 2013 10:41:43 -0500 To: Subject: Issue/Bug Report ******************************************************************************* Name: Roberto Javier Godoy Employer: Universidad Nacional del Litoral mailFrom: rjgodoy@fich.unl.edu.ar Terms_Agreement: I agree Specification: OCL Section: 11.9.1.4 FormalNumber: formal/2012-01-01 Version: 2.3.1 Doc_Year: 2012 Doc_Month: January Doc_Day: 02 Page: 169 Title: Collection::any() violates precondition if the collection is empty Nature: Revision Severity: Significant CODE: 3TMw8 B1: Report Issue Description: Section 11.9.1.4 states that "there must be at least one element fulfilling body, otherwise the result of this IteratorExp is null." And defines source->any(iterator|body) = source->select(iterator | body)->asSequence()->first() However let seq:Sequence=source->select(body)->asSequence() in source->any(body)=seq->at(1) >From section 11.7.5 Âcontext Sequence::first() : T Âpost: result = self->at(1) Âcontext Sequence::at(i : Integer) : T Âpre : i >= 1 and i <= self->size() If there is no element fulfilling body, then seq is empty and the precondition of Sequence::at does not hold because 1 > seq->size(). Related to: Issue 18125 [OCL 2.4] Juergen Boldt Director, Member Services 109 Highland Ave Needham, MA 02494 USA Tel: 781 444 0404 x 132 fax: 781 444 0320 www.omg.org  No virus found in this message. Checked by AVG - www.avg.com Version: 2013.0.2899 / Virus Database: 2641/6132 - Release Date: 02/25/13