11.5.3 String

+ (s : String) : String

self和s的连接。

post: result = self.concat(s)

size() : Integer

self中的字符数。

concat(s : String) : String

self和s的连接。

post: result.size() = self.size() + s.size() --原文中把s 写成了string
post: result.substring(1, self.size() ) = self
post: result.substring(self.size() + 1, result.size() ) = s

substring(lower : Integer, upper : Integer) : String

self中从lower开始包括到upper结束的子字符串。

pre: 1 <= lower
pre: lower <= upper
pre: upper <= self.size()

toInteger() : Integer

将self转换为一个整数值。

toReal() : Real

将self转换为一个实数值。

toUpperCase() : String

使用在当前环境中通过查找oclLocale定义的locale来将self转为大写。否则，返回与self相同的字符串。

toLowerCase() : String

使用在当前环境中通过查找oclLocale定义的locale来将self转为小写。否则，返回与self相同的字符串。

indexOf(s : String) : Integer

查询self中s做为self的字符串的起始位置，或0如果s不是self的子字符串。空串是所有字符串在索引位置1（以及其它索引）的子字符串。

post: self.size() = 0 implies result = 0
post: s.size() = 0 implies result = 1
post: s.size() > 0 and result > 0 implies self.substring(result, result + s.size() - 1) = s

equalsIgnoreCase(s : String) : Boolean

以大小写无关的方式核对self和s是否是等同的。

post: result = (self.toUpperCase() = s.toUpperCase())

at(i : Integer) : String

查询self中位置 i 处的字符。

pre: i > 0
pre: i <= self.size()
post: result = self.substring(i, i)

characters() : Sequence(String)

获得self的字符序列。

post: result = if self.size() = 0 then
                Sequence{}
           else
                Sequence{1..self.size()}->iterate(i; acc : Sequence(String) = Sequence{} |
                                acc->append(self.at(i)))
           endif

toBoolean() : Boolean

将self转换为一个布尔值。

post: result = (self = 'true')

< (s : String) : Boolean

使用在当前环境中通过查找oclLocale定义的locale来判断self是否小于s。

> (s : String) : Boolean

使用在当前环境中通过查找oclLocale定义的locale来判断self是否大于s。

post: result = not (self <= s)

<= (s : String) : Boolean

使用在当前环境中通过查找oclLocale定义的locale来判断self是否小于等于s。

post: result = ((self = s) or (self < s))

>= (s : String) : Boolean

使用在当前环境中通过查找oclLocale定义的locale来判断self是否大于等于s。

post: result = ((self = s) or (self > s))