The lowest precedence operator in a term
if then else.
Note that for an
if then else,
there must always be an
like the C++ operator "
elseterm | logical-term
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.