Ifstatement (conditional branch in a program)
This functionality does not run in MATLAB.
ifcondition_{1}
thencasetrue_{1}
elifcondition_{2}
thencasetrue_{2}
elifcondition_{3}
thencasetrue_{3}
... elsecasefalse
end_if _if(condition_{1}
,casetrue_{1}
,casefalse
)
ifthenelseend_if
allows conditional branching
in a program.
If the Boolean expression condition1
can
be evaluated to TRUE
,
the branch casetrue1
is executed and its result
is returned. Otherwise, if condition2
evaluates
to TRUE
, the branch casetrue2
is
executed and its result is returned etc. If all of the conditions
evaluate to FALSE
, the branch casefalse
is
executed and its result is returned.
All conditions that are evaluated during the execution of the if
statement
must be reducible to either TRUE
or FALSE
.
Conditions may be given by equations or inequalities, combined with the logical operators and
, or
, not
. There is no need to enforce Boolean
evaluation of equations and inequalities via bool
. Implicitly, the if
statement
enforces "lazy" Boolean evaluation via the functions _lazy_and
or _lazy_or
, respectively.
A condition leads to a runtime error if it cannot be evaluated to TRUE
or FALSE
by
these functions. Cf. Example 3.
The keyword end_if
may be replaced by the
keyword end
.
The statement if condition then casetrue else casefalse
end_if
is equivalent to the function call _if(condition,
casetrue, casefalse)
.
The if
statement operates as demonstrated
below:
if TRUE then YES else NO end_if, if FALSE then YES else NO end_if
The else
branch is optional:
if FALSE then YES end_if
if FALSE then if TRUE then NO_YES else NO_NO end_if else if FALSE then YES_NO else YES_YES end_if end_if
Typically, the Boolean conditions are given by equations, inequalities
or Boolean constants produced by system functions such as isprime
:
for i from 100 to 600 do if 105 < i and i^2 <= 17000 and isprime(i) then print(expr2text(i)." is a prime") end_if; if i < 128 then if isprime(2^i  1) then print("2^".expr2text(i)."  1 is a prime") end_if end_if end_for:
Instead of using nested ifthenelse
statements,
the elif
statement can make the source code more
readable. However, internally the parser converts such statements
into equivalent ifthenelse
statements:
hold(if FALSE then NO elif TRUE then YES_YES else YES_NO end_if)
if FALSE then NO else if TRUE then YES_YES else YES_NO end_if end_if
If the condition cannot be evaluated to either TRUE
or FALSE
,
then a runtime error is raised. In the following call, is(x
> 0)
produces UNKNOWN
if no corresponding properties was
attached to x
via assume
:
if is(x > 0) then 1 else 2 end_if
Error: Cannot evaluate to Boolean. [if]
Note that Boolean conditions using <
, <=
, >
, >=
may
fail if they involve symbolic expressions:
if 1 < sqrt(2) then print("1 < sqrt(2)"); end_if
if 10812186006/7645370045 < sqrt(2) then print("10812186006/7645370045 < sqrt(2)"); end_if
if is(10812186006/7645370045 < sqrt(2)) = TRUE then print("10812186006/7645370045 < sqrt(2)"); end_if
This example demonstrates the correspondence between the functional
and the imperative use of the if
statement:
condition := 1 > 0: _if(condition, casetrue, casefalse)
condition := 1 > 2: _if(condition, casetrue, casefalse)
delete condition:

Boolean expressions 

Arbitrary sequences of statements 
Result of the last command executed inside the if
statement.
The empty sequence, null()
is returned if no command
was executed.