Dafny Power User:

Short-Circuit Operators

Short-Circuit Operators

**Abstract.** The boolean operators (“and”, “or”, …) in Dafny are short-circuiting. This means,
for example, that you cannot reverse the operands of “and” and expect your program
to be unchanged. This is well known to programmers. But if you write specifications
in the same programming language, should you not be nervous that “and” no longer
appears to be commutative?

This note points out that the difference lies not in the meaning of the operators, but rather in what expressions are legal in the first place.

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`

.

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.

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.

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

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

[0]Ádám Darvas, Farhad Mehta, and Arsenii Rudich.
Efficient well-definedness checking.
In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors,
*Automated Reasoning, 4th International Joint Conference, IJCAR 2008*,
volume 5195 of *Lecture Notes in Computer Science*, pages 100–115.
Springer, 2008. 🔎