The boolean type bool
has just two values: true
and false
. There are several operators returning booleans, namely the inequalities (<
, <=
, >=
, >
) as well as equality (==
) and disequality (!=
).
Booleans can be tested with conditional expressions b ? e1 : e2
and conditional statements (if
) or in loop exit conditions in for
or while
loops; see statements. The conditional expression b ? e1 : e2
will first evaluate b (which must be of type type
) and then either e1 (if the value of b is true
) or e2 (if the value of b is false
). e1 and e2 must have the same type (which need not be bool
), so that no matter how the test of b turns out, the value of the whole expression has a predictable type.
We can use conditional expression to explain the meaning of several operators that combine booleans.
!b |
b ? false : true |
(negation) |
b1 && b2 |
b1 ? b2 : false |
(conjunction) |
b1 || b2 |
b1 ? true : b2 |
(disjunction) |
Here, logical negation (!
) has higher precedence than conjunction (&&
) which in turn has higher precedence than disjunction (||
). Explicit parentheses are suggested when both conjunction and disjunction are used, to make expressions easier to understand and avoid errors. We can also compare booleans for equality (b1 == b2
) or disequality (b1 != b2
).
The conjunction (&&
) and disjunction (||
) operator have short-circuiting behavior in the following sense:
b1 && b2
does not evaluate b2 if b1 is falseb1 || b2
does not evaluate b2 if b1 is trueYou can see this from the definitions in terms of conditional expressions above.
Here is a simple example where this is important. find(x, A, n)
is intended to return an index i such that A[i] = x or -1 (if no such i exists). We write a partial specification of this behavior, stating that the result i must either be -1, or it is in the range from 0 to n-1 and then A[i] must be equal to x.
int find(int x, int[] A, int n)
//@requires 0 <= n && n <= \length(A);
//@ensures \result == -1 || (0 <= \result && \result < n && A[\result] == x);
{ ... }
Now the array access A[\result]
will always be in bounds, because we never attempt to evaluate A[\result]
unless we have already checked that \result
falls between 0 and the length of the array. Of course, the postcondition (@ensures
) can fail if the (omitted) implementation has a bug, but it can never raise an unexpected exception when trying to access the array.