diff options
| author |  rustanleino <unknown> | 2010-01-07 01:17:04 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-01-07 01:17:04 +0000 |
| commit | 9f5bb9b92d843b3718673545a62791f5049a7d74 (patch) | |
| tree | 76c36c6ee62359302bc9a117fb54d1c4ab3a0b49 /Test | |
| parent | 666463d9fa29f14ea8aaec4d5bc8bd602e0033ba (diff) | |
Dafny: updated to reflect Boogie's new parsing of function arguments
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/BQueue.bpl | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/dafny0/BQueue.bpl b/Test/dafny0/BQueue.bpl index 21c1c58a..77f1efb3 100644 --- a/Test/dafny0/BQueue.bpl +++ b/Test/dafny0/BQueue.bpl @@ -409,7 +409,7 @@ axiom (forall s0: Seq, s1: Seq :: { EqualSeq(s0,s1) } (forall j: int :: { Index(s0,j) } { Index(s1,j) }
0 <= j && j < Length(s0) ==> Index(s0,j) == Index(s1,j)));
-function Take(Seq, howMany: int) returns (Seq);
+function Take(s: Seq, howMany: int) returns (Seq);
axiom (forall s: Seq, n: int :: { Length(Take(s,n)) }
0 <= n ==>
(n <= Length(s) ==> Length(Take(s,n)) == n) &&
@@ -418,7 +418,7 @@ axiom (forall s: Seq, n: int, j: int :: { Index(Take(s,n), j) } 0 <= j && j < n && j < Length(s) ==>
Index(Take(s,n), j) == Index(s, j));
-function Drop(Seq, howMany: int) returns (Seq);
+function Drop(s: Seq, howMany: int) returns (Seq);
axiom (forall s: Seq, n: int :: { Length(Drop(s,n)) }
0 <= n ==>
(n <= Length(s) ==> Length(Drop(s,n)) == Length(s) - n) &&
|