diff options
author | Rustan Leino <unknown> | 2013-04-01 14:28:37 -0700 |
---|---|---|
committer | Rustan Leino <unknown> | 2013-04-01 14:28:37 -0700 |
commit | 7ee036cae0cc6a2d48786f18908f26de37136236 (patch) | |
tree | d8e3965854d7499f754551695f694cee8a7acbe5 /Test/dafny0/Maps.dfy | |
parent | 5152d9cd2fd4cd7258d745ec01324b4b654e1172 (diff) |
Moved resolution of BinaryExpr.ResolveOp until the CheckTypeInference phase, where more type information is known
Refactored ConcreteUpdateStatement to no longer inherit from ConcreteSyntaxStatement.
Fixed numerous places where some recursive checks did not reach.
Diffstat (limited to 'Test/dafny0/Maps.dfy')
-rw-r--r-- | Test/dafny0/Maps.dfy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/dafny0/Maps.dfy b/Test/dafny0/Maps.dfy index 1c245952..b23a3750 100644 --- a/Test/dafny0/Maps.dfy +++ b/Test/dafny0/Maps.dfy @@ -103,13 +103,13 @@ method m7() }
method m8()
{
- var a := map[];
+ var a: map<int,int> := map[];
assert forall i :: i !in a; // check emptiness
var i,n := 0, 100;
while(i < n)
invariant 0 <= i <= n;
invariant forall i | i in a :: a[i] == i * i;
- invariant forall k :: 0 <= k < i <==> k in a;
+ invariant forall k :: 0 <= k < i <==> k in a;
{
a := a[i := i * i];
i := i + 1;
|