2.2 Back to the example

Let us use the example in listing 1 to illustrate this. The expression (i < |a|) (a[i]k) is evaluated as follows:

1.
Evaluate i < |a|.
(a)
If the result is true, continue to the right hand side.
(b)
If the result is false, conclude the whole expression is false, skip the right hand side.
2.
Right hand side: Evaluate a[i]k. The result of this expression becomes the result of the whole conjunction

This means that by the time we evalute the right hand side, a[i]k, we already know that i < |a| must be true. This makes a lot of sense, because if i ≥|a|, then i is already an invalid index into a, which means the right hand side should not be evaluated.

This nice property, however, makes conjunction (and disjunction) not commutable anymore. In other words, the expression (a[i]k) (i < |a|) is no longer equivalent to (i < |a|) (a[i]k). Worse yet, (a[i]k) (i < |a|) breaks the code, too. This is because if we evaluate a[i]k first, it is possible that i ≥|a|, which means a[i] does not exist!