C0 | Documentation
C0 Tutorial C0 and other languages Other references

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