Operations and well-formedness rules


This section contains the operatiins and well-formedness rules of the primitive types.
 

Real

Note that Integer is a subclass of Real, so for each parameter of type Real, you can use an integer as the actual parameter.

+ (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


- : 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
 

String


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.
 

Boolean

or (b : Boolean) : Boolean

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)