Brackets and Conditional Expressions

Brackets

Brackets can be used in the usual way to force an evaluation to occur in a particular order. They can also be used to define names for temporary values, using the keyword let.

For example, to compute the fourth power of x, you could use the expression:

  (let square ^= x * x; square * square)

You can also include assertions within the brackets:

  (assert x ~= 0; x * x)

This tells the verifier (and anyone reading the specification) that x should not be zero at this point.

You can have multiple let and assert parts in one expression, e.g.:

  (let square ^= x * x; assert square >= 0; let fourth ^= square * square; fourth * square )

Conditional expressions

A conditional expression is a special form of bracketed expression, containing two or more guarded expressions.

A guarded expression takes the form:

  [condition]: expression

An ex ample of a complete conditional expression is:

  ( [total > 10]: "lots", [total > 5]: "a few", []: "not enough" )

which may be read: 'If total greater than 10 then "lots", else if total greater than 5 then "a few", else "not enough"'.

When evaluating a conditional expression, the guards are evaluated in order until one evaluates to true; then the corresponding expression is evaluated. The remaining guards and the other expressions are not evaluated. As shown here, the last guard may be empty (i.e. no expression is given within the square brackets), which is equivalent to the condition true and means otherwise (or else).

You may place let and assert parts between the opening round bracket and the first guard.
For example:

  ( let total ^= mine + yours;
    assert total >= mine;
    [total > 10]:
      "lots",
    [total > 5]:
      "a few",
    []:
      "not enough"
  )

This example also demonstrates one possible layout for conditional expressions that do not fit on a single line.

Next:  Calling functions and constructors