11.2. Expressions and Invariants

Expressions are steps typed by only a single Function, which means that their values are evaluations. An expression whose value is an evaluation with results is said to evaluate to those results. They can be steps in any behavior, but a Function, in particular, can designate one of its expression steps as the result expression that gives the value of its result parameter. Expressions can have their own nested parameters, to augment or redefine those of their Functions, including the result parameter. They can also own other expressions and designate a result expression, similarly to a Function.

An expression can be declared as a step using the keyword expr. As for a step, directed features declared in the body of an expression are considered to be parameters of the expression.

Example 1:

function UnaryFunction {in x : Anything; return: Anything;}
function apply {
  in expr fn : UnaryFunction;
  in value : Anything;
  return : Anything = fn( value);
}

Example 2 (shows how an expression can be invoked using a feature chain):

class Stats {
  feature vales[1..*] : Real;
  expr avg { sum(values)/size(values) }
}
feature myStats : Stats {
  redefines feature values = (1.0, 2.0, 3.0);
}
feature myAvg = myStats.avg();

Boolean expressions are expressions whose function is a predicate and, so, evaluate to a Boolean result.

class FuelTank {
  feature fuelLevel : Real;
  feature readonly maxFuelLevel : Real;
  bool isFull { fuelLevel == maxFuelLevel }
}

An invariant, is a Boolean expression that must always evaluate to either true at all times or false at all times. By default, an invariant is asserted to always evaluate to true.

class FuelTank {
  feature fuelLevel : Real;
  feature readonly maxFuelLevel : Real;
  inv { fuelLevel >= 0 & fuelLevel <= maxFuelLevel }
}