diff options
| author |  Unknown <t-jasonk@Z3507288.redmond.corp.microsoft.com> | 2012-05-29 14:56:35 -0700 |
|---|---|---|
| committer | Unknown <t-jasonk@Z3507288.redmond.corp.microsoft.com> | 2012-05-29 14:56:35 -0700 |
| commit | 33be652b4db584a8441f7b1006ceed73eb091be6 (patch) | |
| tree | 6050f3143e35fed1b1053e9c9044a516a539d5da /Test/dafny1/ListContents.dfy | |
| parent | 2e43fe69d087fb75213f67f735a3e85e0278a29f (diff) | |
Dafny: fixed regression tests
Diffstat (limited to 'Test/dafny1/ListContents.dfy')
| -rw-r--r-- | Test/dafny1/ListContents.dfy | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/Test/dafny1/ListContents.dfy b/Test/dafny1/ListContents.dfy index 069ffbde..594be748 100644 --- a/Test/dafny1/ListContents.dfy +++ b/Test/dafny1/ListContents.dfy @@ -86,6 +86,13 @@ class Node<T> { reverse := current;
current := nx;
+ // This makes the verification go faster.
+ assert current != null ==>
+ current.Valid() &&
+ current in old(footprint) && current.footprint <= old(footprint) &&
+ current.footprint !! reverse.footprint &&
+ |old(list)| == |reverse.list| + |current.list| &&
+ (forall i :: 0 <= i && i < |current.list| ==> current.list[i] == old(list)[|reverse.list|+i]);
}
}
}
|