Hi Ron,
The problem is that your ensures clause introduces yet another
q
. Without it, everything verifies:
lemma alltest(A:seq<int>)
{
forall q:nat
ensures q<|A| ==> A[q] ==1
{
assume q<|A| ==> A[q]==1;
}
assert forall q:nat :: q<|A| ==> A[q] ==1;
}
We are writing a comprehensive reference manual for Dafny. For now, here are some notes on the
forall
statement.
The
forall
statement is a
aggregate statement. As such, it performs its body for each of values specified by the bound variables. The body instantiations are performed simultaneously; more precisely, all reads precede writes. The syntax
is as follows (shown here with two bound variables):
forall x: T, y: U | R(x,y,z)
ensures P(x,y,z)
{
Body
}
The types
T
and
U
can be omitted if they can be inferred.
R(x,y,z)
is a boolean expression; if
| R(x,y,z)
is omitted, the expression defaults to
true
. Optionally,
x: T, y: U | R(x,y,z)
can be enclosed in parentheses. As a degenerate case, the statement allows no bound variables (and, in that case, no
| R(x,y,z)
), which is sometimes useful to hide the proof of the
ensures
condition (in the future, I plan to introduce a version of the
assert
statement that does this instead).
P(x,y,z)
is a boolean expression. Multiple
ensures
clauses have the same effect as conjoining their conditions.
Body
is a list of statements.
There are two basic version of the
forall
statement, one executable and one ghost.
In the executable version of the
forall
statement,
ensures
clauses are not allowed and the
Body
must be one assignment statement. Note that the
forall
statement is not a loop. In particular, no loop invariant is required to reason about it. However, the
forall
statement can perform the duties of simple loops. For example, the following
forall
statement initializes all elements of a real matrix:
forall i, j | 0 <= i < m.Length0 && 0 <= j < m.Length1 {
m[i,j] := 0.0;
}
Reads are performed before writes, so the following
forall
statement rotates the elements of an array:
forall i | 0 <= i < a.Length {
a[i] := a[(i + 1) % a.Length];
}
Just like in multiple-assignment statements, the left-hand sides of the various body instantiations must denote different l-values (unless the corresponding right-hand sides are equal). In the executable version of the
forall
statement, range expression
R(x,y,z)
combined with the types of the bound variables must be within a finite range, thus ensuring that the
forall
statement will terminate.
The ghost version of the
forall
statement corresponds to the logic rule of "universal introduction": by proving a property
P(x)
for an arbitrary
x
, one obtains the universally quantified fact
forall x :: P(x)
. Here, the
Body
can be any list of (ghost) statements that lead to the verification of the given
ensures
conditions. If the
Body
consists of a single lemma call and the
ensures
clause of the
forall
statement is omitted, then Dafny automatically uses the lemma's
ensures
clauses as the
ensures
clauses of the
forall
statement. Similarly, if
Body
consists of a single
calc
statement and the
ensures
clause is omitted, then Dafny will use the conclusion of the
calc
statement (that is, its first line connected with its last line) as the
ensures
condition.
I hope this explanation will help.
Program safely,
Rustan