This section contains the operatiins and well-formedness rules of
the primitive types.
+ (r : Real) : Real
The value of the addition of self and r.
- (r : Real) : Real
The value of the subtraction of r from self.
* (r : Real) : Real
The value of the multiplication of self and r.
- : Real
The negative value of self.
/ (r : Real) : Real
The value of self divided by r.
abs() : Real
The absolute value of self.
post: if self < 0 then result = - self else result = self endif
floor() : Integer
The largest integer which is less than or equal to self.
post: (result <= self) and (result + 1 > self)
round() : Integer
The integer which is closest to self. When there are two such integers, the largest one.
post: ((self - result).abs() < 0.5) or ((self - result).abs() = 0.5 and (result > self))
max(r : Real) : Real
The maximum of self and r.
post: if self >= r then result = self else result = r endif
min(r : Real) : Real
The minimum of self and r.
post: if self <= r then result = self else result = r endif
< (r : Real) : Boolean
True if self is less than r.
> (r : Real) : Boolean
True if self is greater than r.
post: result = not (self <= r)
<= (r : Real) : Boolean
True if self is less than or equal to r.
post: result = ((self = r) or (self < r))
>= (r : Real) : Boolean
True if self is greater than or equal to r.
post: result = ((self
= r) or (self > r))
- : Integer
The negative value of self.
+ (i : Integer) : Integer
The value of the addition of self and i.
- (i : Integer) : Integer
The value of the subtraction of i from self.
* (i : Integer) : Integer
The value of the multiplication of self and i.
/ (i : Integer) : Real
The value of self divided by i.
abs() : Integer
The absolute value of self.
post: if self < 0 then result = - self else result = self endif
div( i : Integer) : Integer
The number of times that i fits completely within self.
pre : i <> 0
post: if self / i >=
0 then result = (self / i).floor()
else result = -((-self/i).floor())
endif
mod( i : Integer) : Integer
The result is self modulo i.
post: result = self - (self.div(i) * i)
max(i : Integer) : Integer
The maximum of self an i.
post: if self >= i then result = self else result = i endif
min(i : Integer) : Integer
The minimum of self an i.
post: if self <= i
then result = self else result = i endif
size() : Integer
The number of characters in self.
concat(s : String) : String
The concatenation of self and s.
post: result.size() =
self.size() + string.size()
post: result.substring(1,
self.size() ) = self
post: result.substring(self.size()
+ 1, result.size() ) = s
substring(lower : Integer, upper : Integer) : String
The sub-string of self starting at character number lower, up to and including character number upper. Character numbers run from 1 to self.size().
pre: 1 <= lower
pre: lower <= upper
pre: upper <= self.size()
toInteger() : Integer
Converts self to an Integer value.
toReal() : Real
Converts self to a Real value.
True if either self or b is true.
xor (b : Boolean) : Boolean
True if either self or b is true, but not both.
post: (self or b) and not (self = b)
and (b : Boolean) : Boolean
True if both b1 and b are true.
not : Boolean
True if self is false.
post: if self then result = false else result = true endif
implies (b : Boolean) : Boolean
True if self is false, or if self is true and b is true.
post: (not self) or (self
and b)