6.1.1 If then else

The lowest precedence operator in a term is if then else. Note that for an if then else, there must always be an else part, like the C++ operator "?:".

term ::= if term then term else term
        | logical-term

In an if then else term, the first term must have sort Bool, and the other terms must have the same sort, which is the sort of the whole term. The meaning is just what you would expect. See page 162 of [Guttag-Horning93] for a formal statement.

Note that in LSL, there are no undefined terms; so technically, even a term such as div(5,0) would have a value. But with the use of if then else, one can ignore the values of such terms. For example, the following is equivalent to x' = 3.

if true then x' = 3 else x' = div(5,0)

Go to the first, previous, next, last section, table of contents.