diff options
author | 2011-05-21 18:15:17 -0700 | |
---|---|---|
committer | 2011-05-21 18:15:17 -0700 | |
commit | 9dbf2a6ce1e130f634c27da7bc300001e28aedaf (patch) | |
tree | 929593e6a181ba2cfb4fe94d5157f73f3667fae2 /Test/dafny0/DTypes.dfy | |
parent | 1aa1ca45fc066c9f8d94eeff1a2dc140c49db393 (diff) |
Dafny:
* started rewriting parsing of qualified identifiers in expressions
* annoyingly, had to introduce AST nodes for concrete syntax
* previous syntax for invoking datatype constructors: #List.Cons(h, t)
new syntax: List.Cons(h, t)
or, if only one datatype has a constructor named Cons: Cons(h, t)
* Removed type parameters for datatype constructors from the grammar
* Helped Test/VSI-Benchmarks/b4.dfy along with a couple of assertions (previously, its proving performance was highly varied)
Diffstat (limited to 'Test/dafny0/DTypes.dfy')
-rw-r--r-- | Test/dafny0/DTypes.dfy | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy index 2f59db73..b402c335 100644 --- a/Test/dafny0/DTypes.dfy +++ b/Test/dafny0/DTypes.dfy @@ -80,7 +80,7 @@ datatype Data { }
function G(d: Data): int
- requires d != #Data.Lemon;
+ requires d != Data.Lemon;
{
match d
case Lemon => G(d)
@@ -144,19 +144,19 @@ class DatatypeInduction<T> { method IntegerInduction_Succeeds(a: array<int>)
requires a != null;
requires a.Length == 0 || a[0] == 0;
- requires (forall j :: 1 <= j && j < a.Length ==> a[j] == a[j-1]+2*j-1);
+ requires forall j :: 1 <= j && j < a.Length ==> a[j] == a[j-1]+2*j-1;
{
// The following assertion can be proved by induction:
- assert (forall n {:induction} :: 0 <= n && n < a.Length ==> a[n] == n*n);
+ assert forall n {:induction} :: 0 <= n && n < a.Length ==> a[n] == n*n;
}
method IntegerInduction_Fails(a: array<int>)
requires a != null;
requires a.Length == 0 || a[0] == 0;
- requires (forall j :: 1 <= j && j < a.Length ==> a[j] == a[j-1]+2*j-1);
+ requires forall j :: 1 <= j && j < a.Length ==> a[j] == a[j-1]+2*j-1;
{
// ...but the induction heuristics don't recognize the situation as one where
// applying induction would be profitable:
- assert (forall n :: 0 <= n && n < a.Length ==> a[n] == n*n); // error reported
+ assert forall n :: 0 <= n && n < a.Length ==> a[n] == n*n; // error reported
}
}
|