0. The Well-Definedness Rule

In Dafny, a.Length gives the length of the array referenced by a and 5/x gives the integer quotient of 5 and x. But what if a is null or if x is 0, what do these expressions mean then? The Dafny verifier checks that you are never in a situation where you have to rely on what these expressions evaluate to for such operand values. So, in a legal Dafny program, expressions are known to be defined. This allows the verifier to do meaningful reasoning and allows the compiler to assume the absence of run-time failures. I'll call this the Well-Definedness Rule.

To enforce the Well-Definedness Rule, the Dafny verifier checks that every expression you write down is well-defined in every context where that expression could possibly be used. For example, the well-definedness of a.Length is a != null and the well-definedness of 5/x is x != 0.

1. Short-circuiting

The boolean operators &&, ||, ==>, and <== are short-circuiting in Dafny. This notion is commonly described in terms of how an expression is evaluated at run time, namely: evaluation proceeds left-to-right (or right-to-left in the case of <==), but an operand is evaluated only if the operands evaluated so far do not already determine the value of the expression. In this way, if the first operand determines the value of the expression (as evaluating the first operand of && to false does), then the evaluation of the second operand is omitted.

The meaning of the boolean operators are the same in Dafny as in logic.

Hold it! How can that be? Conjunction (“and”) in logic is symmetric (that is, A && B is the same as B && A) and short-circuiting is inherently asymmetric. How can a short-circuiting operator have the same meaning as in logic? Here's how: Short-circuiting affects the well-definedness of expressions, not their meaning when defined.

So, I should have said: Expressions with boolean operators are not always defined in Dafny. But when they are defined, their meaning is the same in Dafny as in logic.

2. Example: commutativity of and

In logic,

x != 0 && 5/x == 1

is the very same thing as

5/x == 1 && x != 0

This is also true in Dafny, but only in situations where these are well-defined.

x != 0 is always well-defined and 5/x == 1 is well-defined when x is non-0. That is, the well-definedness of x != 0 is true and the well-definedness of 5/x == 1 is x != 0.

Let me use WDe to denote the well-definedness of an expression e. So, WDx != 0 is true and WD5/x == 1 is x != 0.

For conjunction, we have that WDe0 && e1 is

WDe0 && (e0 ==> WDe1)

That is, while the left argument has to be well-defined, the right argument only has to be well-defined when the left argument evaluates to true.

So, WDx != 0 && 5/x == 1 is

true && (x != 0 ==> x != 0)

which simplifies to true. In contrast, WD5/x == 1 && x != 0 is

x != 0 && (5/x == 1 ==> true)

which simplifies to x != 0.

Summarizing the example, conjunction in logic is symmetric. This is also true in Dafny, provided that both ways of writing the expression are well-defined. As the example shows, the first conjunction is always well-defined, whereas the other is well-defined only when x != 0. So, if you're in a situation where you don't know if x != 0 holds or not, you're better off writing the first of these conjunctions.

3. Example: contrapositive

The contrapositive of the implication A ==> B is !B ==> !A, that is, the implication with the arguments reversed and negated. In logic, these two implications are equivalent. This is also true in Dafny, provided both expressions are defined.

As an example, consider the expression a != null ==> a.Length > 0. We have that WDa != null ==> a.Length > 0 is

true && (a != null ==> a != null)

which simplifies to true. For the contrapositive of the implication, we have that WDa.Length <= 0 ==> a == null is

a != null && (a.Length <= 0 ==> true)

which simplifies to a != null.

In Dafny, we can only talk about the meaning of expressions if they are well-defined. As we just worked out, the first of these implications is always well-defined whereas the other is well-defined when a != null. So, in any context where a != null is known to hold, the two implications have the same meaning and you can use them interchangeably. But if there's a possibility that a != null might not hold, then the first implication is still defined (and thus you can start to talk about what value the expression will evaluate to), whereas the second implication is not well-defined (and thus is flagged as an error by the Dafny verifier).

4. Symmetric well-definedness

As a final remark, well-definedness of boolean operands in Dafny is defined to match the notion of short-circuiting. This is well understood by programmers. Indeed, no programmer in their right mind would even think of ever writing

p.x < 1000 && p != null

but would write

p != null && p.x < 1000

As we have seen, this gives rise to an asymmetric definition of well-definedness. But this is not the only way to define well-definedness. For more information, see an article by Darvas, Mehta, and Rudich [0].