diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-04-21 17:32:52 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-04-21 17:32:52 -0700 |
| commit | d367c34ddf96cf77559e86e4311b4fad564c3262 (patch) | |
| tree | 4b65e2cf37db96668b154de5228be84ddfe3d3b5 /Test | |
| parent | ec5c7538c19c214bd76d2004b55abf7cf3c6b0b3 (diff) | |
Dafny: Fix parsing of if-then-else expressions, and don't require parentheses around forall/exists expressions
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny1/ExtensibleArray.dfy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/dafny1/ExtensibleArray.dfy b/Test/dafny1/ExtensibleArray.dfy index 4ceca552..089a72c4 100644 --- a/Test/dafny1/ExtensibleArray.dfy +++ b/Test/dafny1/ExtensibleArray.dfy @@ -17,11 +17,11 @@ class ExtensibleArray<T> { more in Repr && more.Repr <= Repr && this !in more.Repr && elements !in more.Repr &&
more.Valid() &&
|more.Contents| != 0 &&
- (forall j :: 0 <= j && j < |more.Contents| ==>
+ forall j :: 0 <= j && j < |more.Contents| ==>
more.Contents[j] != null && more.Contents[j].Length == 256 &&
more.Contents[j] in Repr && more.Contents[j] !in more.Repr &&
more.Contents[j] != elements &&
- (forall k :: 0 <= k && k < |more.Contents| && k != j ==> more.Contents[j] != more.Contents[k]))) &&
+ forall k :: 0 <= k && k < |more.Contents| && k != j ==> more.Contents[j] != more.Contents[k]) &&
// length
M == (if more == null then 0 else 256 * |more.Contents|) &&
|