Dafny Power User:

Statement versus Expression Syntax

Statement versus Expression Syntax

**Abstract.** This note describes some constructs that exist in both a statement form and an
expression form in Dafny. It points out the syntactic similarities and differences
between the two forms, and discusses related constructs.

Dafny distinguishes between *statements* and *expressions*. For example, the body of a
`method`

is a statement whereas the body of a `function`

is an expression.
A statement can assign to local variables, allocate and mutate objects
in the heap, use loops in control flow, and be nondeterministic. An expression
cannot do any of those things. Instead, it can bind values to bound variables,
read values in the heap, use recursion, and is always deterministic.
Syntactically, most statements are terminated with a semi-colon and sometimes
a sequence of statements is surrounded by curly braces. A few expressions contain
semi-colons, but never at the end, and an expression can be surrounded by round
parentheses.

Let's take a look at some constructs that exist in both a statement form and an expression form.

Of constructs that exist in both statement and expression form, the
*conditional* (`if`

) is probably the most common, and it is also the one
with the most conspicuous difference between the two forms.

The conditional statement is the `if`

statement, which
has a “then” branch and an optional “else” branch.
The “then” branch is always a block statement, which is necessarily
surrounded by curly braces. The “else” branch, if present, is either
a block statement or another `if`

statement.

For example, the following statement declares local variables
`min`

and `max`

that are assigned according to the relative sizes of `x`

and `y`

:

```
var min, max;
if x < y {
min, max := x, y;
} else {
min, max := y, x;
}
```

Notice that `min`

and `max`

are declared before the `if`

statement (Dafny will
infer the types of these two variables), which means they are still in scope
after the whole `if`

statement. If these variables were instead declared inside
each branch, they would go out of scope at the curly brace that ends each
respective block statement.

The conditional expression is the `if`

-`then`

-`else`

expression. Unlike the
`if`

statement, the expression form uses the keyword `then`

to separate the
guard from the “then” branch, and always requires and explicit “else” branch.
For example, an expression that returns the smaller of `x`

and `y`

is:

`if x < y then x else y`

Such expressions can be used as right-hand sides of assignments to local variables:

`var min, max := if x < y then x else y, if x < y then y else x;`

For this example, we can also use a single `if`

-`then`

-`else`

expression
where each branch results in a pair. We can assign that pair to a variable,
and then assign the pair's components to `min`

and `max`

:

```
var minmax := if x < y then (x,y) else (y,x);
var min, max := minmax.0, minmax.1;
```

The following shows an example of nested and cascaded `if`

statements:

```
var middle;
if x < y {
if y < z {
middle := y;
} else if z < x {
middle := x;
} else {
middle := z;
}
} else {
if x < z {
middle := x;
} else if z < y {
middle := y;
} else {
middle := z;
}
}
```

And here is the analogous program using conditional expressions:

```
var middle :=
if x < y then
if y < z then y else if z < x then x else z
else
if x < z then x else if z < y then y else z;
```

For statements, there are some additional forms of conditionals. Because these forms allow nondeterminism, there statements do exist in an analogous expression form. The next few subsections describe these additional conditional statements.

One additional form of conditional statements is the * if-case statement*.
Instead of two mutually exclusive branches, the

`if`

-`case`

statement provides
any number of branches (cases, alternatives), and their conditions need not be mutually
exclusive. Syntactically, the `if`

-`case`

statement follows the keyword `if`

with
ones or more branches of the form
`case Guard => Body`

where `Guard`

is an expression and `Body`

is a list of statements.

For example, the computation of `min`

/`max`

can be written as follows:

```
var min, max;
if
case x <= y =>
min, max := x, y;
case y <= x =>
min, max := y, x;
```

Note that `<=`

is the “at most” (or, some say “less than or equal to”)
operator, whereas `=>`

is the piece of syntax that separates the
guard and body of each case.

The `if`

-`case`

statement picks any one of the cases whose guard evaluates
to `true`

. The ordering of the cases is not relevant.
In the example above, if `x`

and `y`

are equal, then the choice
of which `case`

to execute is nondeterminstic. For this example, it so
happens that both cases have the same effect if `x`

and `y`

are equal,
but that need not be so. Not having to specify which branch to take when
the choice is irrelevant frees the programmer's mind and, arguably, results
in a cleaner, more symmetric, and more abstract program.

Each `case`

gives rise to a new block scope, despite the fact that the body
is a list of statements, not a block statement. In other words, any local
variables declared in one `case`

go out of scope where the `case`

ends.

The body of a `case`

continues until the next `case`

begins or until the
enclosing block ends. If you want to end the last `case`

sooner, you could
surround the entire `if`

-`case`

statement with a pair of curly braces, but
that doesn't look so nice. Therefore, Dafny optionally allows the set of
cases to be enclosed in a pair of curly braces, like this:

```
var min, max;
if {
case x <= y =>
min, max := x, y;
case y <= x =>
min, max := y, x;
}
```

An `if`

-`case`

statement can have any number of branches. For example:

```
var middle;
if {
case x <= y <= z => middle := y;
case z <= y <= x => middle := y;
case y <= x <= z => middle := x;
case z <= x <= y => middle := x;
case y <= z <= x => middle := z;
case x <= z <= y => middle := z;
}
```

As I mentioned, if more than one guard evaluates to `true`

, Dafny may choose
to execute any one of the the corresponding bodies (but only one!). What if
none of the guards evaluates to `true`

? That is not allowed, and the verifier
will report an error if it cannot prove that at least one case applies.

When Dafny is used as a modeling language, one may want to write down several
statements that can be chosen between indiscriminately. This can be done by
writing `*`

in place of the guard expression in the common `if`

statement.

For example, the effect of the statement

```
if * {
S;
} else if * {
T;
} else {
U;
}
```

is to execute one of the statements `S`

, `T`

, or `U`

, but you can never predict
which one of those statements will be chosen.

Such an indiscriminate choice can also be written using an `if`

-`case`

statement:

```
if
case true => S;
case true => T;
case true => U;
```

Finally, both the common `if`

statement and the `if`

-`case`

statement allow guards
to introduce a variable with some constraints. These are called *binding guards*.

For example, suppose you want to perform an operation to an arbitrary even
number in a given set, unless the set contains no even number, in which case you
want to do something else.
One way to accomplish this is to write an `if`

statement whose then branch uses
an *assign-such-that statement* to pick such an element:

```
if exists x :: x in S && x % 2 == 0 {
var x :| x in S && x % 2 == 0;
ProcessEven(x);
} else {
ProcessEmpty();
}
```

But there is a lot of duplication between the existential quantifier in the guard and the assign-such-that statement in the then branch. With a binding guard, the same program can be written as follows:

```
if x :| x in S && x % 2 == 0 {
ProcessEven(x);
} else {
ProcessEmpty();
}
```

This statement introduces `x`

and picks as its value any value satisfying the
condition following the `:|`

. If no such `x`

exists, the else branch is executed.
The bound variable `x`

is in scope only in the then branch.

Similarly, suppose you want to pick an even number from a set and apply some
operation to it, or pick an odd number from the set and apply some other operation
to it, or do something else if the set contains neither an even nor an odd number.
Then you can use an `if`

-`case`

statement with binding guards:

```
if
case x :| x in S && x % 2 == 0 =>
ProcessEven(x);
case x :| x in S && x % 2 == 1 =>
ProcessOdd(x);
case S == {} =>
ProcessEmpty();
```

Note that if `S`

contains both even and odd numbers, then Dafny may pick either of
the first two cases.

Another branching construct is `match`

, which also comes in a statement form and in
an expression form. The syntax of these two are identical, except that each body of
the former is a list of statements where each body of the latter is an expression.
These have the forms

```
match s
case A(x) =>
StmtList0;
case B(y) =>
StmtList1;
case C(z) =>
StmtList2;
```

and

```
match s
case A(x) => Expr0
case B(y) => Expr1
case C(z) => Expr2
```

respectively.

What follows the keyword `case`

is a *pattern*, which looks like an expression
built of datatype constructors and bound variables. For example, consider the
standard datatype definition for a list, parameterized by an element type `T`

:

`datatype List<T> = Nil | Cons(T, List<T>)`

The following expression returns the minimum of `2`

and the length of a list `xs`

:

```
match xs
case Nil => 0
case Cons(x, Nil) => 1
case Cons(x, Cons(y, ys)) => 2
```

Unlike in several other programming languages, the cases of a `match`

in Dafny are unordered.
A bound variable that is not used can be replaced by an underscore, `_`

.
So, the `match`

expression above can be written equivalently as

```
match xs
case Cons(_, Nil) => 1
case Cons(_, Cons(_, _)) => 2
case Nil => 0
```

Analogously to the `if`

-`case`

statement, each `case`

of a `match`

statement
is implicitly a lexical scope. In other words, any local variables declared in
one `case`

goes out of scope at the end of that branch.

Also as for the `if`

-`case`

statement, each `case`

of a `match`

goes as far as
possible, but not past another `case`

. To end a case early, the set of cases can be
enclosed in a pair of curly braces. For example:

```
match xs
case Cons(_, ys) =>
match ys {
case Cons(_, _) => 2
case Nil => 1
}
case Nil => 0
```

Note that curly braces, not parentheses, are used in this way for both `match`

statements and `match`

expressions. One can, of course, also surround an entire
`match`

expression with parentheses, so the expression above can be written
equivalently as:

```
match xs
case Cons(_, ys) =>
(match ys
case Cons(_, _) => 2
case Nil => 1)
case Nil => 0
```

In some situations, it may also be possible to simply reorder the cases for the same effect:

```
match xs
case Nil => 0
case Cons(_, ys) =>
match ys
case Nil => 1
case Cons(_, _) => 2
```

The statement that introduces a local variable has the form:

`var x: int := 17;`

The type decoration "`: int`

“ is needed only if Dafny cannot infer the
type, so it is typically omitted.
The assignment of an initial value, here ”`:= 17`

", can also be omitted,
if the initial value of the variable is irrelevant. (If the variable is used
before the program explicitly assigns to it, Dafny will initialize the variable
to an arbitrary value of its type.) The variable introduced stays in scope
until the current lexical scope ends (typically at the next close-curly-brace).

A `var`

statement can introduce several variables. If so, any type decoration
acts only on the variable it follows. That is, you can think of `:`

as having
higher binding power than the `,`

that separates the variable names.
If an initial assignment is used, it must give a value to all variables being
declared. For example,

`var a, b: bool, c := 13, true, 8.29;`

declares an integer variable `a`

, a boolean variable `b`

, and a real-valued
variable `c`

.

The following example introduces three local variables, `z`

, `x`

, and `y`

,
and arranges in a complicated way to set `z`

to `0`

(where `k`

is some integer
variable in the enclosing scope):

```
var z;
var x, y := k, k;
z := x - y;
```

There is a form of the `var`

statement in expressions: the *let expression*.
The variables introduced by let expressions are usually called
*bound variables* or *let-bound variables*. The syntax of the let expression
is like the `var`

statement, but followed by an expression. For example, the expression

```
var w := 5; w + w
```

returns `10`

. If you're used to functional programming, you may choose to
read this statement as “let” (`var`

) `w`

“be” (`:=`

) `5`

“in” (`;`

) `w + w`

.

The syntax intentionally mimics that of the `var`

statement, to deemphasize
the distinction between statements and expressions. For example, the statement
that assigns to `z`

above can be written with a let expression:

```
var z :=
var x, y := k, k;
x - y;
```

except that, here, the variables `x`

and `y`

are only in scope in the body
of the let expression (which ends at the semi-colon); in the statement above,
`x`

and `y`

are introduced as local variables, which remain in scope until the
end of the lexical block. Note that the first semi-colon is a
separator in the let expression, whereas the second semi-colon terminates the
`var`

statement.

Local variables can be modified by assignment statements. In contrast,
let-bound variables are immutable. In this light, we think of a let expression
as *binding* a value to each of its let-bound variables. Whereas the right-hand side
of the `:=`

in a `var`

statement gives initial values to the local variable,
the right-hand side of the `:=`

in a let expression provides *defining values*
for the let-bound variables.
A syntactic difference between the `var`

statement and let expression is that a let
expression must always include the `:=`

and the accompanying defining expressions.

The relation between `var`

statements and let expressions is analogous to
the relation between a `case`

in a `match`

statement and a `case`

in a
`match`

expression. Recall, for the `match`

constructs, each `case`

takes
the shape

`case Pattern => StmtList;`

or

`case Pattern => Expr`

respectively. Analogously, `var`

statements and let expressions take the
respective shapes

`var x := Expr; StmtList;`

or

`var x := Expr; Expr`

Many constructs in Dafny come in two manifestations: *compiled* or *ghost*.
A ghost construct is used in specifications to reason
about the correctness of the program, but is erased by the compiler and has
no run-time cost. Local variables and let expressions come in both manifestations.
The ones we saw above were all compiled manifestations. To declare local
variables or let-bound variables as ghost, simply precede the `var`

keyword
with `ghost`

.

For example,

```
var m := 20;
ghost var n := m + 3;
```

introduces a compiled variable `m`

and a ghost variable `n`

.

Dafny makes sure that ghost variables (and other ghost constructs) really can
be erased by the compiler without changing the meaning of the program. One of
the checks it performs is that the values of
compiled variables never depend on ghost variables. For example, the following
declaration of `n`

as a compiled variable is not legal, because the use the value
of a ghost variable in an assignment to a compiled variable:

```
ghost var m := 20;
var n := m + 3; // error: illegal to assign a ghost to a compiled variable
```

When a `var`

statement or let expression omits the `ghost`

keyword, all variables
the statement introduces are declared as compiled. And when the `ghost`

keyword is
present, all variables the statement introduces are declared as ghost. There is
one exception to this
rule. The exception applies when a `var`

statement that omits the `ghost`

keyword
gives a method call as the right-hand side.
Then, any local variable that corresponds to a ghost out-parameter of the method
called is implicitly declared as ghost, and if the method itself is ghost, then
all of the local variables are implicitly declared as ghost.

For example, consider a method with two out-parameters, one compiled and one ghost:

`method M() returns (x: int, ghost y: int)`

The statement

`var a, b := M();`

declares `a`

to be a compiled local variable and `b`

to be a ghost
local variable. If the statement explicitly uses the `ghost`

keyword, as in

`ghost var a, b := M();`

then both `a`

and `b`

are declared to be ghost local variables.

In a `var`

statement and let expression, the left-hand side of `:=`

need not be
a list of variables, but can be a list of *patterns*, just like the patterns in
the cases of a `match`

construct. This has the effect of deconstructing the right-hand
side of `:=`

(that is, the initializing or defining expressions) and then assigning
the new variables.

For example, using the datatype definition `List`

from above, the `var`

statement

`var Cons(a, Cons(b, Nil)) := E;`

introduces two variables, `a`

and `b`

, and sets these to the first two elements
of the list `E`

. The value denoted by the right-hand side must match the pattern in
the left-hand side, and this is enforced by the verifier. In the example, `E`

must
denote a list whose length is exactly `2`

.

Just like in `match`

patterns, any variable that is not needed can be replaced by
an underscore. For example,

```
var Cons(_, Cons(b, _)) := E;
```

introduces `b`

and initializes it to the second element of the list `E`

, where `E`

is allowed to have more than two elements.

To discard a result from the right-hand side, use an underscore as the corresponding
actual out-parameter. For example, if `P`

is a method with one out-parameter,

`var _ := P();`

calls `P()`

and then discards its result. This is also allowed if `P`

is a function,
but then there's not much point in making the function call at all.

The `var`

statements and let expressions we've seen so far are precise about
what value to assign or bind to the new variables. There's is a cousin to these
constructs that instead prescribes a set of values, any one of which may be
picked at run-time as the value assigned. It is the *assign-such-that* statement
(in statement form) and the *let-such-that* expression (in expression form).

For example, the assign-such-that statement

```
var x :| x in S;
```

introduces local variable `x`

and says to set it to any value that satisfies the
predicate `x in S`

. In other words, this statement sets `x`

to some value in `S`

.
(The verifier will complain for this example statement if it cannot prove `S`

to
be nonempty.)

Syntactically, the difference between an ordinary assignment and an assign-such-that
construct is that the former uses `:=`

whereas the latter uses `:|`

. Also, in the
ordinary assignment, the variables introduced are not in scope in the right-hand
side, where the variables introduced are in scope in the right-hand side of the
assign-such-that constructs. Like the `var`

statement and let expression, the
such-that forms can introduce multiple variables, but the left-hand side is always
a list of variables, never patterns.

Here is an example `var`

statement with an assign-such-that statement that introduces
three new variables, `b`

, `s`

, and `t`

. It requires that either `S`

is nonempty
or `N`

is strictly positive.

`var b, s, t :| (b ==> s in S) && (!b ==> 0 <= t < N);`

The assign-such-that constructs give rise to a proof obligation that there exists
some value for each of the new variables that satisfies the right-hand side.
For the example above, the proof obligation thus amounts to that `S`

is nonempty.
A Dafny compiler may impose additional restrictions on the right-hand side, because
it may not always be clever enough to generate executable code that is guaranteed
to, in finite time, find values for the variables.

The assign-such-that statement and let-such-that expression are the same, but there is an additional restriction on compiled let-such-that expressions. The restriction stems from the fact that expressions in Dafny are always deterministic, that is, if you evaluate an expression twice in the same state, you will get the same value. This is important in order to let the verifier reason about “obvious” properties like

`E == E`

Statements, on the other hand, can be nondeterministic, so assign-such-that statements may return different values each time they are executed:

```
var x :| x in S;
var y :| y in S;
assert x == y; // this condition is NOT guaranteed, unless |S| == 1
```

Dafny's guarantee that let-such-that expressions be deterministic
(within each run of the program) is unproblematic for ghost expressions, but the
same guarantee for *compiled* let-such-that expressions would incur too high of
a run-time cost (see [1]). Instead, Dafny restricts compiled
such-that-expressions to those that *uniquely* specify the values of its variables.
For example, if `S`

is a nonempty set of integers, the compiled expression

```
var x :| x in S && forall y :: y in S ==> x <= y;
x
```

is legal and evaluates to the smallest element in `S`

. Unfortunately, this
restriction on compiled let-such-that expressions is sometimes more harsh than
one would like.

Let-bound variables get their value at the time of declaration, but local variables
can be subsequently updated with assignment statements or assign-such-that statements.
These are like the assignments that provide the initial value of the local variables,
except that patterns in the left-hand side are allowed only when the local variables
are introduced, not in subsequent assignments.^{0}

Generally, statements contain expressions, but not the other way around.
With one exception: the *statement expression*. It has the form `S; E`

,
where `S`

is one of several ghost statements and `E`

is an expression.
The expression `S; E`

evaluates to `E`

. That is, statement `S`

does not
affect the value of the expression. The role of `S`

is to provide information
that will help prove the *well-formedness* of `E`

.

For example, suppose there is a function `F`

and a lemma `AboutF`

that
tells us something about the value returned by `F`

:

```
function method F(x: int): int
lemma AboutF(x: int)
requires 0 <= x
ensures 0 < F(x)
```

In the example, the lemma `AboutF`

, which can be used if `x`

is non-negative,
says that `F(x)`

returns a positive value. Now, consider the following
statement:

```
if 0 <= y && 10 / F(y) == 2 { // error: possible division by zero
// ...
}
```

Without further information, Dafny is unable to prove the absence of
division-by-zero in the guard of this `if`

statement. To help the verifier
along, we can use the lemma. To do that, we might try calling the
lemma just before the `if`

statement:

```
AboutF(y); // error: precondition violation
if 0 <= y && 10 / F(y) == 2 {
// ...
}
```

But that doesn't work, because in that context, it could be that `y`

is
negative. By using a statement expression, we can insert the lemma call
just where we need it:

```
if 0 <= y && 10 / (AboutF(y); F(y)) == 2 {
// ...
}
```

A statement expression accepts five kinds of statements: lemma calls and
`assert`

, `assume`

, `reveal`

, and `calc`

statements.

There's a restriction on the lemma calls in statement expressions: the lemma
must not have any out-parameters.^{1} This may be frustrating when it
occasionally pops up.

As an example, consider the following declarations:

```
// Some property that integers may have
predicate P(k: int)
// A lemma that, for every x, shows---by returning a witness---the
// existence of a k satisfying P(k)
lemma MyLemma(x: int) returns (k: int)
ensures P(k)
// Two functions that need the P property
function method G(x: int, ghost k: int): int
requires P(k)
function method H(x: int): int
requires exists k :: P(k)
```

It would be nice to be able to write an expression

`var k := MyLemma(x); G(x, k)`

or to write an expression

`var _ := MyLemma(x); H(x)`

when the out-parameter does not need to be named. But the restriction forbids these.

There are workarounds. They are rather clumsy, but they show how various expressions discussed in this note can be combined to produce the desired result.

For the latter case, a workaround is the expression

```
assert exists k :: P(k) by {
var _ := MyLemma(x);
}
H(x)
```

The former is similar, but also uses a let-such-that expression to obtain a
name for the value whose existence is proved by the first `assert`

:

```
assert exists k :: P(k) by {
var _ := MyLemma(x);
}
ghost var k :| P(k);
G(x, k)
```

Note that this let-such-that expression is ghost, so the restriction that
`k`

must be determined uniquely does not apply.

Dafny makes a distinction between statements and expressions, but the syntactic similarities I've discussed in this note make it less of a burden to remember what to write where. As a final example, consider the following (rather contrived) method and function for computing the same thing:

```
method DoItByMethod(xs: List<int>) returns (r: nat)
{
match xs
case Nil =>
return 0;
case Cons(x, _) =>
var square := x * x;
AboutF(square);
return F(square);
}
function method DoItByFunction(xs: List<int>): nat
{
match xs
case Nil =>
0
case Cons(x, _) =>
var square := x * x;
AboutF(square);
F(square)
}
```

To be technical about it, the method uses a `match`

statement, a `var`

statement
with a local variable, a lemma call, and the final function call that computes
the result, whereas the function uses a `match`

expression, a let expression
with a let-bound variable, a statement expression featuring a lemma call, and
the final function call.

But when you're in the midst of it, there's no need to dwell on those fine distinctions!

I thank Matthias Schlaipfer for useful feedback on this note.

[1]K. Rustan M. Leino. “Compiling Hilbert’s $\varepsilon$ Operator.” In *LPAR-20. 20th International Conferences on Logic for Programming,
Artificial Intelligence and Reasoning — Short Presentations*, edited by Ansgar Fehnker, Annabelle McIver, Geoff Sutcliffe, and Andrei Voronkov, 35:106–118. EPiC Series in Computer Science. EasyChair. Dec. 2015. 🔎