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 | 0ba294b71f0ed7f805bb475ca67aa229dcb973d8 (patch) | |
| tree | e343e12934a0beab01519b876aaeafbc92b6bcaf /Test/dafny1/ExtensibleArray.dfy | |
| parent | f84b171441e3a171f39fd402be5e08dbcab0b8b9 (diff) | |
Dafny: Fix parsing of if-then-else expressions, and don't require parentheses around forall/exists expressions
Diffstat (limited to 'Test/dafny1/ExtensibleArray.dfy')
| -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|) &&
|