Booleans

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 false
• b1 || b2 does not evaluate b2 if b1 is true

You 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.