Issue 17220: OCL String::indexOf (ocl2-rtf)
Source: Model Driven Solutions (Dr. Edward Willink, ed(at)willink.me.uk)
Nature: Uncategorized Issue
Severity: 
Summary: The description of String::indexOf() states "No string is a substring of the empty string.".


This modifies the axiom that every string is a substring of itself. It would appear that the empty string has got confused with null.


An extension of the library with startsWith and endsWith operations would require the modified axiom to be accommodated making corner cases equivalently strange.


This modified axiom is not observed by other String libraries such as the java.lang.String.


Suggest: Replace the text:


"The empty string is considered to be a substring of every string but the empty string, at index 1. No string is a substring of the empty string."


by


"The empty string is a substring of every string at index 1 (and also at all other indexes)."


Resolution: yes
Revised Text: In 11.5.3 String indexOf replace
The empty string is considered to be a substring of every string but the empty string, at index 1. No string is a substring of the empty string.
by
The empty string is a substring of every string at index 1 (and also at all other indexes).
and
post: s.size() = 0 and self.size() > 0 implies result = 1
by
post: s.size() = 0 implies result = 1
Actions taken:
March 9, 2012: received issue
December 23, 2013: closed issue
Discussion: 

End of Annotations:=====

m: Ed Willink <ed@willink.me.uk>
To: issues@omg.org
Subject: OCL String::indexOf


The description of String::indexOf() states "No string is a substring of the empty string.".


This modifies the axiom that every string is a substring of itself. It would appear that the empty string has got confused with null.


An extension of the library with startsWith and endsWith operations would require the modified axiom to be accommodated making corner cases equivalently strange.


This modified axiom is not observed by other String libraries such as the java.lang.String.


Suggest: Replace the text:


"The empty string is considered to be a substring of every string but the empty string, at index 1. No string is a substring of the empty string."


by


"The empty string is a substring of every string at index 1 (and also at all other indexes)."


    Regards


        Ed Willink