Generic types, like A<T,U>, consist of a type constructor, here A, and type parameters, here T and U.
Type constructors are not first-class entities in Dafny, they are always used syntactically to construct
type names; to do so, they must have the requisite number of type parameters, which must be either concrete types, type parameters, or
a generic type instance.
However, those type parameters do not always have to be explicit; Dafny can often infer what they ought to be. For example, here is a fully parameterized function signature:
type List<T>
function Elements<T>(list: List<T>): set<T>However, Dafny also accepts
type List<T>
function Elements(list: List): setIn the latter case, Dafny knows that the already defined types set and List each take one type parameter
so it fills in <T> (using some unique type parameter name) and then determines that the function itself needs
a type parameter <T> as well.
Dafny also accepts
type List<T>
function Elements<T>(list: List): setIn this case, the function already has a type parameter list. List and set are each known to need type parameters,
so Dafny takes the first n parameters from the function signature and applies them to List and set, where n (here 1) is the
number needed by those type constructors.
It never hurts to simply write in all the type parameters, but that can reduce readability. Omitting them in cases where Dafny can intuit them makes a more compact definition.
This process is described in more detail with more examples in this paper: http://leino.science/papers/krml270.html.
Signatures of methods, functions, fields (except const fields with a
RHS), and datatype constructors have to declare the types of their
parameters. In other places, types can be omitted, in which case
Dafny attempts to infer them. Type inference is "best effort" and may
fail. If it fails to infer a type, the remedy is simply for the
program to give the type explicitly.
Despite being just "best effort", the types of most local variables, bound variables, and the type parameters of calls are usually inferred without the need for a program to give the types explicitly. Here are some notes about type inference:
- With some exceptions, type inference is performed across a whole method body. In some cases, the information needed to infer a local variable's type may be found after the variable has been declared and used. For example, the nonsensical program
```dafny
method M(n: nat) returns (y: int)
{
var a, b;
for i := 0 to n {
if i % 2 == 0 {
a := a + b;
}
}
y := a;
}
```
uses a and b after their declarations. Still, their types are
inferred to be int, because of the presence of the assignment y := a;.
A more useful example is this:
```dafny
class Cell {
var data: int
}
method LastFive(a: array<int>) returns (r: int)
{
var u := null;
for i := 0 to a.Length {
if a[i] == 5 {
u := new Cell;
u.data := i;
}
}
r := if u == null then a.Length else u.data;
}
```
Here, using only the assignment u := null; to infer the type of
u would not be helpful. But Dafny looks past the initial
assignment and infers the type of u to be Cell?.
- The primary example where type inference does not inspect the entire context before giving up on inference is when there is a member lookup. For example,
```dafny
datatype List<T> = Nil | Cons(T, List<T>)
method Tutone() {
assert forall pair :: pair.0 == 867 && pair.1 == 5309 ==> pair == (867, 5309); // error: members .0 and .1 not found
assert forall pair: (int, int) :: pair.0 == 867 && pair.1 == 5309 ==> pair == (867, 5309);
}
```
In the first quantifier, type inference fails to infer the type of
pair before it tries to look up the members .0 and .1, which
results in a "type of the receiver not fully determined" error. The
remedy is to provide the type of pair explicitly, as is done in the
second quantifier.
(In the future, Dafny may do more type inference before giving up on the member lookup.)
- If type parameters cannot be inferred, then they can be given explicitly in angle brackets. For example, in
```dafny
datatype Option<T> = None | Some(T)
method M() {
var a: Option<int> := None;
var b := None; // error: type is underspecified
var c := Option<int>.None;
var d := None;
d := Some(400);
}
```
the type of b cannot be inferred, because it is underspecified.
However, the types of c and d are inferred to be Option<int>.
Here is another example:
```dafny
function EmptySet<T>(): set<T> {
{}
}
method M() {
var a := EmptySet(); // error: type is underspecified
var b := EmptySet();
b := b + {2, 3, 5};
var c := EmptySet<int>();
}
```
The type instantiation in the initial assignment to a cannot
be inferred, because it is underspecified. However, the type
instantiation in the initial assignment to b is inferred to
be int, and the types of b and c are inferred to be
set<int>.
- Even the element type of
newis optional, if it can be inferred. For example, in
```dafny
method NewArrays()
{
var a := new int[3];
var b: array<int> := new [3];
var c := new [3];
c[0] := 200;
var d := new [3] [200, 800, 77];
var e := new [] [200, 800, 77];
var f := new [3](_ => 990);
}
```
the omitted types of local variables are all inferred as
array<int> and the omitted element type of each new is inferred
to be int.
-
In the absence of any other information, integer-looking literals (like
5and7) are inferred to have typeint(and not, say,bv128orORDINAL). -
Many of the types inferred can be inspected in the IDE.
After1 type inference, Dafny revisits the program and makes a final decision about which statements are to be compiled, and which statements are ghost. The ghost statements form what is called the ghost context of expressions.
These statements are determined to be ghost:
assert,assume,reveal, andcalcstatements.- The body of the
byof anassertstatement. - Calls to ghost methods, including lemmas.
if,match, andwhilestatements with condition expressions or alternatives containing ghost expressions. Their bodies are also ghost.forloops whose start expression contains ghost expressions.- Variable declarations if they are explicitly ghost or if their respective right-hand side is a ghost expression.
- Assignments or update statement if all updated variables are ghost.
forallstatements, unless there is exactly one assignment to a non-ghost array in its body.
These statements always non-ghost:
The following expressions are ghost, which is used in some of the tests above:
- All specification expressions
- All calls to functions and predicates marked as
ghost - All variables, constants and fields declared using the
ghostkeyword
Note that inferring ghostness can uncover other errors, such as updating non-ghost variables in ghost contexts.
For example, if f is a ghost function, in the presence of the following code:
var x := 1;
if(f(x)) {
x := 2;
}Dafny will infer that the entire if is ghost because the condition uses a ghost function,
and will then raise the error that it's not possible to update the non-ghost variable x in a ghost context.
Recursive functions are a core part of computer science and mathematics. Roughly speaking, when the definition of such a function spells out a terminating computation from given arguments, we may refer to it as a well-founded function. For example, the common factorial and Fibonacci functions are well-founded functions.
There are also other ways to define functions. An important case regards the definition of a boolean function as an extreme solution (that is, a least or greatest solution) to some equation. For computer scientists with interests in logic or programming languages, these extreme predicates are important because they describe the judgments that can be justified by a given set of inference rules (see, e.g., [@CamilleriMelham:InductiveRelations; @Winskel:FormalSemantics; @LeroyGrall:CoinductiveBigStep; @Pierce:SoftwareFoundations; @NipkowKlein:ConcreteSemantics]).
To benefit from machine-assisted reasoning, it is necessary not just to understand extreme predicates but also to have techniques for proving theorems about them. A foundation for this reasoning was developed by Paulin-Mohring [@PaulinMohring:InductiveCoq] and is the basis of the constructive logic supported by Coq [@Coq:book] as well as other proof assistants [@BoveDybjerNorell:BriefAgda; @SwamyEtAl:Fstar2011]. Essentially, the idea is to represent the knowledge that an extreme predicate holds by the proof term by which this knowledge was derived. For a predicate defined as the least solution, such proof terms are values of an inductive datatype (that is, finite proof trees), and for the greatest solution, a coinductive datatype (that is, possibly infinite proof trees). This means that one can use induction and coinduction when reasoning about these proof trees. These extreme predicates are known as, respectively, least predicates and greatest predicates. Support for extreme predicates is also available in the proof assistants Isabelle [@Paulson:CADE1994] and HOL [@Harrison:InductiveDefs].
Dafny supports both well-founded functions and extreme predicates. This section describes the difference in general terms, and then describes novel syntactic support in Dafny for defining and proving lemmas with extreme predicates. Although Dafny's verifier has at its core a first-order SMT solver, Dafny's logical encoding makes it possible to reason about fixpoints in an automated way.
The encoding for greatest predicates in Dafny was described previously [@LeinoMoskal:Coinduction] and is here described in the section about datatypes.
To define a function
where boolean function, that is, if
For example, the common Fibonacci function over the natural numbers can be defined by the equation
With the understanding that the argument
The fact that the function being defined occurs on both sides of the equation causes concern that we might not be defining the function properly, leading to a logical inconsistency. In general, there could be many solutions to an equation like the general equation or there could be none. Let's consider two ways to make sure we're defining the function uniquely.
A standard way to ensure that the general equation has a unique solution in
then we want to check
For example, to check the decrement condition for
Note that we are entitled to use the antecedent
A well-founded function is often thought of as "terminating" in the sense
that the recursive depth in evaluating
With
So that we can later see how inductive proofs are done in Dafny, let's prove that
for any
We don't need to exclude the possibility of the general equation having multiple solutions---instead, we can just be clear about which one of them we want. Let's explore this, after a smidgen of lattice theory.
For any complete lattice
In particular, if false true),
then the set of predicates over any domain
Speaking about the set of solutions in
To conclude our little excursion into lattice theory, we have that, under the
proviso of false more often than any other) and a greatest solution (that
is, a function that returns true more often than any other).
When discussing extreme solutions, let's now restrict our attention to boolean functions
(that is, with
Here is a running example. Consider the following equation,
where
This equation has four solutions in
The first of these is the least solution and the last is the greatest solution.
In the literature, the definition of an extreme predicate is often given as a set of inference rules. To designate the least solution, a single line separating the antecedent (on top) from conclusion (on bottom) is used:
Through repeated applications of such rules, one can show that the predicate holds for
a particular value. For example, the derivation, or proof tree,
to the left in the proof tree figure shows that
When inference rules are to designate the greatest solution, a thick line is used:
In this case, proof trees are allowed to be infinite.
For example, the left-hand example below shows a finite proof tree that uses the inductive rules to establish
Note that derivations may not be unique. For example, in the case of the greatest
solution for
In general, one cannot evaluate whether or not an extreme predicate holds for some
input, because doing so may take an infinite number of steps. For example, following
the recursive calls in the definition the EvenNat equation to try to evaluate
For any
These functions are called the iterates of false, let true, and let a superscript on
For any solution
In other words, every
By the prefix postfix result, we also have that
Let's consider two examples, both involving function
The main technique for establishing that
The technique for going in the other direction, proving something from an established
Let's prove
Here's how we do the proof formally using the least exists definition. We massage the general form of our proof goal:
The last line can be proved by induction over false, so our goal holds trivially.
If
We can think of a predicate
To go in the other direction, to establish a predicate defined as a greatest solution,
like
Let's prove
For anyone who may have felt that the intuitive proof felt too easy, here is a formal proof using the greatest forall definition, which relies only on induction. We massage the general form of our proof goal:
The last line can be proved by induction over
Although this section has considered only well-founded functions and extreme
predicates, it is worth mentioning that there are additional ways of making sure that
the set of solutions to the general equation is nonempty. For example, if all calls to
This section explains with examples the support in Dafny for well-founded functions, extreme predicates, and proofs regarding these, building on the concepts explained in the previous section.
Declarations of well-founded functions are unsurprising. For example, the Fibonacci function is declared as follows:
function fib(n: nat): nat
{
if n < 2 then n else fib(n-2) + fib(n-1)
}Dafny verifies that the body (given as an expression in curly braces) is well defined.
This includes decrement checks for recursive (and mutually recursive) calls. Dafny
predefines a well-founded relation on each type and extends it to lexicographic tuples
of any (fixed) length. For example, the well-founded relation false.
Using a decreases clause, the programmer can specify the term in this predefined
order. When a function definition omits a decreases clause, Dafny makes a simple
guess. This guess (which can be inspected by hovering over the function name in the
Dafny IDE) is very often correct, so users are rarely bothered to provide explicit
decreases clauses.
If a function returns bool, one can drop the result type : bool and change the
keyword function to predicate.
Dafny has lemma declarations, as described in Section 6.3.3:
lemmas can have pre- and postcondition specifications and their body is a code block.
Here is the lemma we stated and proved in the fib example in the previous section:
lemma FibProperty(n: nat)
ensures fib(n) % 2 == 0 <==> n % 3 == 0
{
if n < 2 {
} else {
FibProperty(n-2); FibProperty(n-1);
}
}
function fib(n: nat): nat
{
if n < 2 then n else fib(n-2) + fib(n-1)
}The postcondition of this lemma (keyword ensures) gives the proof
goal. As in any program-correctness logic (e.g.,
[@Hoare:AxiomaticBasis]), the postcondition must
be established on every control path through the lemma's body. For
FibProperty, I give the proof by
an if statement, hence introducing a case split. The then branch is empty, because
Dafny can prove the postcondition automatically in this case. The else branch
performs two recursive calls to the lemma. These are the invocations of the induction
hypothesis and they follow the usual program-correctness rules,
namely: the precondition must hold at the call site, the call must terminate, and then
the caller gets to assume the postcondition upon return. The "proof glue" needed
to complete the proof is done automatically by Dafny.
Dafny features an aggregate statement using which it is possible to make (possibly
infinitely) many calls at once. For example, the induction hypothesis can be called
at once on all values n' smaller than n:
forall n' | 0 <= n' < n {
FibProperty(n');
}For our purposes, this corresponds to strong induction. More
generally, the forall statement has the form
forall k | P(k)
ensures Q(k)
{ Statements; }Logically, this statement corresponds to universal introduction: the body proves that
Q(k) holds for an arbitrary k such that P(k), and the conclusion of the forall statement
is then forall statement is
a single call (or calc statement), the ensures clause is inferred and can be omitted,
like in our FibProperty example.
Lemma FibProperty is simple enough that its whole body can be replaced by the one
forall statement above. In fact, Dafny goes one step further: it automatically
inserts such a forall statement at the beginning of every lemma [@Leino:induction].
Thus, FibProperty can be declared and proved simply by:
lemma FibProperty(n: nat)
ensures fib(n) % 2 == 0 <==> n % 3 == 0
{ }
function fib(n: nat): nat
{
if n < 2 then n else fib(n-2) + fib(n-1)
}Going in the other direction from universal introduction is existential elimination,
also known as Skolemization. Dafny has a statement for this, too:
for any variable x and boolean expression Q, the
assign such that statement x :| Q; says to assign to x a value such that Q
will hold. A proof obligation when using this statement is to show that there
exists an x such that Q holds. For example, if the fact
k :| 100 <= fib(k) < 200; will assign to k some value (chosen arbitrarily)
for which fib(k) falls in the given range.
The previous subsection explained that a predicate declaration introduces a
well-founded predicate. The declarations for introducing extreme predicates are
least predicate and greatest predicate. Here is the definition of the least and
greatest solutions of g and G:
least predicate g[nat](x: int) { x == 0 || g(x-2) }
greatest predicate G[nat](x: int) { x == 0 || G(x-2) }When Dafny receives either of these definitions, it automatically declares the corresponding
prefix predicates. Instead of the names g#[k] and G#[k], respectively, that is, the name of
the extreme predicate appended with #, and the subscript is given as an argument in
square brackets. The definition of the prefix predicate derives from the body of
the extreme predicate and follows the form in the least approx definition and the greatest approx definition.
Using a faux-syntax for illustrative purposes, here are the prefix
predicates that Dafny defines automatically from the extreme
predicates g and G:
predicate g#[_k: nat](x: int) { _k != 0 && (x == 0 || g#[_k-1](x-2)) }
predicate G#[_k: nat](x: int) { _k != 0 ==> (x == 0 || G#[_k-1](x-2)) }The Dafny verifier is aware of the connection between extreme predicates and their prefix predicates, the least exists definition and the greatest forall definition.
Remember that to be well defined, the defining functor of an extreme predicate must be monotonic, and for the least exists definition and the greatest forall definition to hold, the functor must be continuous. Dafny enforces the former of these by checking that recursive calls of extreme predicates are in positive positions. The continuity requirement comes down to checking that they are also in continuous positions: that recursive calls to least predicates are not inside unbounded universal quantifiers and that recursive calls to greatest predicates are not inside unbounded existential quantifiers [@Milner:CCS; @LeinoMoskal:Coinduction].
From what has been presented so far, we can do the formal proofs for the example about the least solution and the example about the greatest solution. Here is the former:
least predicate g[nat](x: int) { x == 0 || g(x-2) }
greatest predicate G[nat](x: int) { x == 0 || G(x-2) }
lemma EvenNat(x: int)
requires g(x)
ensures 0 <= x && x % 2 == 0
{
var k: nat :| g#[k](x);
EvenNatAux(k, x);
}
lemma EvenNatAux(k: nat, x: int)
requires g#[k](x)
ensures 0 <= x && x % 2 == 0
{
if x == 0 { } else { EvenNatAux(k-1, x-2); }
}Lemma EvenNat states the property we wish to prove. From its
precondition (keyword requires) and
the least exists definition, we know there is some k that will make the condition in the
assign-such-that statement true. Such a value is then assigned to k and passed to
the auxiliary lemma, which promises to establish the proof goal. Given the condition
g#[k](x), the definition of g# lets us conclude k != 0 as well as the disjunction
x == 0 || g#[k-1](x-2). The then branch considers the case of the first disjunct,
from which the proof goal follows automatically. The else branch can then assume
g#[k-1](x-2) and calls the induction hypothesis with those parameters. The proof
glue that shows the proof goal for x to follow from the proof goal with x-2 is
done automatically.
Because Dafny automatically inserts the statement
forall k', x' | 0 <= k' < k && g#[k'](x') {
EvenNatAux(k', x');
}at the beginning of the body of EvenNatAux, the body can be left empty and Dafny
completes the proof automatically.
Here is the Dafny program that gives the proof from the example of the greatest solution:
least predicate g[nat](x: int) { x == 0 || g(x-2) }
greatest predicate G[nat](x: int) { x == 0 || G(x-2) }
lemma Always(x: int)
ensures G(x)
{ forall k: nat { AlwaysAux(k, x); } }
lemma AlwaysAux(k: nat, x: int)
ensures G#[k](x)
{ }While each of these proofs involves only basic proof rules, the setup feels a bit clumsy, even with the empty body of the auxiliary lemmas. Moreover, the proofs do not reflect the intuitive proofs described in the example of the least solution and the example of the greatest solution. These shortcomings are addressed in the next subsection.
The proofs we just saw follow standard forms:
use Skolemization to convert the least predicate into a prefix predicate for some k
and then do the proof inductively over k; respectively,
by induction over k, prove the prefix predicate for every k, then use
universal introduction to convert to the greatest predicate.
With the declarations least lemma and greatest lemma, Dafny offers to
set up the proofs
in these standard forms. What is gained is not just fewer characters in the program
text, but also a possible intuitive reading of the proofs. (Okay, to be fair, the
reading is intuitive for simpler proofs; complicated proofs may or may not be intuitive.)
Somewhat analogous to the creation of prefix predicates from extreme predicates, Dafny
automatically creates a prefix lemma L# from each "extreme lemma" L. The pre-
and postconditions of a prefix lemma are copied from those of the extreme lemma,
except for the following replacements:
- for a least lemma, Dafny looks in the precondition to find calls (in positive, continuous
positions) to least predicates
P(x)and replaces these withP#[_k](x); - for a greatest lemma,
Dafny looks in the postcondition to find calls (in positive, continuous positions)
to greatest predicates
P(including equality among coinductive datatypes, which is a built-in greatest predicate) and replaces these withP#[_k](x). In each case, these predicatesPare the lemma's focal predicates.
The body of the extreme lemma is moved to the prefix lemma, but with
replacing each recursive
call L(x) with L#[_k-1](x) and replacing each occurrence of a call
to a focal predicate
P(x) with P#[_k-1](x). The bodies of the extreme lemmas are then replaced as shown
in the previous subsection. By construction, this new body correctly leads to the
extreme lemma's postcondition.
Let us see what effect these rewrites have on how one can write proofs. Here are the proofs of our running example:
least predicate g(x: int) { x == 0 || g(x-2) }
greatest predicate G(x: int) { x == 0 || G(x-2) }
least lemma EvenNat(x: int)
requires g(x)
ensures 0 <= x && x % 2 == 0
{ if x == 0 { } else { EvenNat(x-2); } }
greatest lemma Always(x: int)
ensures G(x)
{ Always(x-2); }Both of these proofs follow the intuitive proofs given in the example of the least solution and the example of the greatest solution. Note that in these simple examples, the user is never bothered with either prefix predicates nor prefix lemmas---the proofs just look like "what you'd expect".
Since Dafny automatically inserts calls to the induction hypothesis at the beginning of
each lemma, the bodies of the given extreme lemmas EvenNat and
Always can be empty and Dafny still completes the proofs.
Folks, it doesn't get any simpler than that!
The Dafny language semantics ensures that any use (read) of a variable (or constant, parameter, object field, or array element) gives a value of the variable's type. It is easy to see that this property holds for any variable that is declared with an initializing assignment. However, for many useful programs, it would be too strict to require an initializing assignment at the time a variable is declared. Instead, Dafny ensures the property through auto-initialization and rules for definite assignment.
As explained in section 5.3.1, each type in Dafny is one of the following:
- auto-init type: the type is nonempty and the compiler has some way to emit code that constructs a value
- nonempty type: the type is nonempty, but the compiler does not know how perform automatic initialization
- possibly empty type: the type is not known for sure to have a value
For a variable of an auto-init type, the compiler can initialize the variable automatically. This means that the variable can be used immediately after declaration, even if the program does not explicitly provide an initializing assignment.
In a ghost context, one can an imagine a "ghost" that initializes variables. Unlike the compiler, such a "ghost" does not need to emit code that constructs an initializing value; it suffices for the ghost to know that a value exists. Therefore, in a ghost context, a variable of a nonempty type can be used immediately after declaration.
Before a variable of a possibly empty type can be used, the program must initialize it. The variable need not be given a value when it is declared, but it must have a value by the time it is first used. Dafny uses the precision of the verifier to reason about the control flow between assignments and uses of variables, and it reports an error if it cannot assure itself that the variable has been given a value.
The elements of an array must be assured to have values already in the statement that allocates the array. This is achieved in any of the following four ways:
- If the array is allocated to be empty (that is, one of its dimensions is requested to be 0), then the array allocation trivially satisfies the requirement.
- If the element type of the array is an auto-init type, then nothing further is required by the program.
- If the array allocation occurs in a ghost context and the element type is a nonempty type, then nothing further is required by the program.
- Otherwise, the array allocation must provide an initialization display or an initialization function. See section 5.10 for information about array initialization.
The fields of a class must have values by the end of the first phase of each constructor (that is, at
the explicit or implicit new; statement in the constructor). If a class has a compiled field that is
not of an auto-init type, or if it has a ghost field of a possibly empty type, then the class is required
to declare a(t least one) constructor.
The yield-parameters of an iterator turn into fields of the corresponding iterator class, but there
is no syntactic place to give these initial values. Therefore, every compiled yield-parameter must be of
auto-init types and every ghost yield-parameter must be of an auto-init or nonempty type.
For local variables and out-parameters, Dafny supports two definite-assignment modes:
- A strict mode (the default, which is
--relax-definite-assignment=false; or/definiteAssignment:4in the legacy CLI), in which local variables and out-parameters are always subject to definite-assignment rules, even for auto-initializable types. - A relaxed mode (enabled by the option
--relax-definite-assignment; or/definiteAssignment:1in the legacy CLI), in which the auto-initialization (or, for ghost variables and parametes, nonemptiness) is sufficient to satisfy the definite assignment rules.
A program using the strict mode can still indicate that it is okay with an arbitrary value of a variable x
by using an assignment statement x := *;, provided the type of x is an auto-init type (or, if x is
ghost, a nonempty type). (If x is of a possibly nonempty type, then x := *; is still allowed, but it
sets x to a value of its type only if the type actually contains a value. Therefore, when x is of
a possibly empty type, x := *; does not count as a definite assignment to x.)
Note that auto-initialization is nondeterministic. Dafny only guarantees that each value it assigns to
a variable of an auto-init type is some value of the type. Indeed, a variable may be auto-initialized
to different values in different runs of the program or even at different times during the same run of
the program. In other words, Dafny does not guarantee the "zero-equivalent value" initialization that
some languages do. Along these lines, also note that the witness value provided in some subset-type
declarations is not necessarily the value chosen by auto-initialization, though it does esstablish that
the type is an auto-init type.
In some programs (for example, in some test programs), it is desirable to avoid nondeterminism.
For that purpose, Dafny provides an --enforce-determinism option. It forbids use of any program
statement that may have nondeterministic behavior and it disables auto-initialization.
This mode enforces definite assignments everywhere, going beyond what the strict mode does by enforcing
definite assignment also for fields and array elements. It also forbids the use of iterator declarations
and constructor-less class declarations. It is up to a user's build process to ensure that
--enforce-determinism is used consistently throughout the program. (In the legacy CLI, this
mode is enabled by /definiteAssignment:3.)
This document, which is intended for developers of the Dafny tool itself, has more detail on auto-initialization and how it is implemented.
Finally, note that --relax-definite-assignment=false is the default in the command-based CLI,
but, for backwards compatibility, the relaxed rules (`/definiteAssignment:1) are still the default
in the legacy CLI.
The well-founded order relations for a variety of built-in types in Dafny are given in the following table:
type of X and x |
x strictly below X |
|---|---|
bool |
X && !x |
int |
x < X && 0 <= X |
real |
x <= X - 1.0 && 0.0 <= X |
set<T> |
x is a proper subset of X |
multiset<T> |
x is a proper multiset-subset of X |
seq<T> |
x is a consecutive proper sub-sequence of X |
map<K, V> |
x.Keys is a proper subset of X.Keys |
| inductive datatypes | x is structurally included in X |
| reference types | x == null && X != null |
| coinductive datatypes | false |
| type parameter | false |
| arrow types | false |
Also, there are a few relations between the rows in the table above. For example, a datatype value x sitting inside a set that sits inside another datatype value X is considered to be strictly below X. Here's an illustration of that order, in a program that verifies:
datatype D = D(s: set<D>)
method TestD(dd: D) {
var d := dd;
while d != D({})
decreases d
{
var x :| x in d.s;
d := x;
}
}During verification, when Dafny knows that a universal quantifier is true, such as when verifying the body of a function that has the requires clause forall x :: f(x) == 1, it may instantiate the quantifier. Instantiation means Dafny will pick a value for all the variables of the quantifier, leading to a new expression, which it hopes to use to prove an assertion. In the above example, instantiating using 3 for x will lead to the expression f(3) == 1.
For each universal quantifier, Dafny generates rules to determine which instantiations are worthwhile doing. We call these rules triggers, a term that originates from SMT solvers. If Dafny can not generate triggers for a specific quantifier, it falls back to a set of generic rules. However, this is likely to be problematic, since the generic rules can cause many useless instantiations, leading to verification timing out or failing to proof a valid assertion. When the generic rules are used, Dafny emits a warning telling the user no triggers were found for the quantifier, indicating the Dafny program should be changed so Dafny can find triggers for this quantifier.
Here follows the approach Dafny uses to generate triggers based on a quantifier. Dafny finds terms in the quantifier body where a quantified variable is used in an operation, such as in a function application P(x), array access a[x], member accesses x.someField, or set membership tests x in S. To find a trigger, Dafny must find a set of such terms so that each quantified variable is used. You can investigate which triggers Dafny finds by hovering over quantifiers in the IDE and looking for 'Selected triggers', or by using the options --show-tooltips when using the LCI.
There are particular expressions which, for technical reasons, Dafny can not use as part of a trigger. Among others, these expression include: match, let, arithmetic operations and logical connectives. For example, in the quantifier forall x :: x in S ⇐⇒ f(x) > f(x+1), Dafny will use x in S and f(x) as trigger terms, but will not use x+1 or any terms that contain it. You can investigate which triggers Dafny can not use by hovering over quantifiers in the IDE and looking for 'Rejected triggers', or by using the options --show-tooltips when using the LCI.
Besides not finding triggers, another problematic situation is when Dafny was able to generate triggers, but believes the triggers it found may still cause useless instantiations because they create matching loops. Dafny emits a warning when this happens, indicating the Dafny program should be changed so Dafny can find triggers for this quantifier that do not cause matching loops.
To understand matching loops, one needs to understand how triggers are used. During a single verification run, such as verifying a method or function, Dafny maintains a set of expressions which it believes to be true, which we call the ground terms. For example, in the body of a method, Dafny knows the requires clauses of that method hold, so the expressions in those will be ground terms. When Dafny steps through the statements of the body, the set of ground terms grows. For example, when an assignment var x := 3 is evaluated, a ground term x == 3 will be added. Given a universal quantifier that's a ground term, Dafny will try to pattern match its triggers on sub-expressions of other ground terms. If the pattern matches, that sub-expression is used to instantiate the quantifier.
Dafny makes sure not to perform the exact same instantiation twice. However, if an instantiation leads to a new term that also matches the trigger, but is different from the term used for the instantiation, the quantifier may be instantiated too often, an event we call a matching loop. For example, given the ground terms f(3) and forall x {f(x)} :: f(x) + f(f(x)), where {f(x)} indicates the trigger for the quantifier, Dafny may instantiate the quantifier using 3 for x. This creates a new ground term f(3) + f(f(3)), of which the right hand side again matches the trigger, allowing Dafny to instantiate the quantifier again using f(3) for x, and again and again, leading to an unbounded amount of instantiations.
Even existential quantifiers need triggers. This is because when Dafny determines an existential quantifier is false, for example in the body of a method that has requires !exists x :: f(x) == 2, Dafny will use a logical rewrite rule to change this existential into a universal quantifier, so it becomes requires forall x :: f(x) != 2. Before verification, Dafny can not determine whether quantifiers will be determined to be true or false, so it must assume any quantifier may turn into a universal quantifier, and thus they all need triggers. Besides quantifiers, comprehensions such as set and map comprehensions also need triggers, since these are modeled using universal quantifiers.
Dafny may report 'Quantifier was split into X parts'. This occurs when Dafny determines it can only generate good triggers for a quantifier by splitting it into multiple smaller quantifiers, whose aggregation is logically equivalent to the original one. To maintain logical equivalence, Dafny may have to generate more triggers than if the split had been done manually in the Dafny source file. An example is the expression forall x :: P(x) && (Q(x) =⇒ P(x+1)), which Dafny will split into
forall x {P(x)} {Q(x)} :: P(x) &&
forall x {(Q(x)} :: Q(x) =⇒ P(x+1)Note the trigger {Q(x)} in the first quantifier, which was added to maintain equivalence with the original quantifier. If the quantifier had been split in source, only the trigger {P(x)} would have been added for forall x :: P(x).
Footnotes
-
Ghost inference has to be performed after type inference, at least because it is not possible to determine if a member access
a.brefers to a ghost variable until the type ofais determined. ↩