diff options
Diffstat (limited to 'Test/dafny0/DTypes.dfy')
| -rw-r--r-- | Test/dafny0/DTypes.dfy | 38 |
1 files changed, 19 insertions, 19 deletions
diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy index c8c893a0..9891c040 100644 --- a/Test/dafny0/DTypes.dfy +++ b/Test/dafny0/DTypes.dfy @@ -1,11 +1,11 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /autoTriggers:1 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
class C {
var n: set<Node>;
method M(v: Stack)
- requires v != null;
+ requires v != null
{
var o: object := v;
assert o !in n; // should be known from the types involved
@@ -28,12 +28,12 @@ class C { method A1(a: CP<int,C>)
{
var x: object := a;
- assert (forall b: CP<int,Stack> :: x == b ==> b == null); // follows from type antecedents
+ assert (forall b: CP<int,Stack> {:nowarn} :: x == b ==> b == null); // follows from type antecedents
}
var a2x: set<CP<C,Node>>;
method A2(b: set<CP<Node,C>>)
- requires null !in b;
+ requires null !in b
{
var x: set<object> := a2x;
var y: set<object> := b;
@@ -81,7 +81,7 @@ class CP<T,U> { datatype Data = Lemon | Kiwi(int)
function G(d: Data): int
- requires d != Data.Lemon;
+ requires d != Data.Lemon
{
match d
case Lemon => G(d)
@@ -101,28 +101,28 @@ class DatatypeInduction<T> { }
method Theorem0(tree: Tree<T>)
- ensures 1 <= LeafCount(tree);
+ ensures 1 <= LeafCount(tree)
{
assert (forall t: Tree<T> :: 1 <= LeafCount(t));
}
// also make sure it works for an instantiated generic datatype
method Theorem1(bt: Tree<bool>, it: Tree<int>)
- ensures 1 <= LeafCount(bt);
- ensures 1 <= LeafCount(it);
+ ensures 1 <= LeafCount(bt)
+ ensures 1 <= LeafCount(it)
{
assert (forall t: Tree<bool> :: 1 <= LeafCount(t));
assert (forall t: Tree<int> :: 1 <= LeafCount(t));
}
method NotATheorem0(tree: Tree<T>)
- ensures LeafCount(tree) % 2 == 1;
+ ensures LeafCount(tree) % 2 == 1
{
assert (forall t: Tree<T> :: LeafCount(t) % 2 == 1); // error: fails for Branch case
}
method NotATheorem1(tree: Tree<T>)
- ensures 2 <= LeafCount(tree);
+ ensures 2 <= LeafCount(tree)
{
assert (forall t: Tree<T> :: 2 <= LeafCount(t)); // error: fails for Leaf case
}
@@ -140,22 +140,22 @@ class DatatypeInduction<T> { // ----- here is a test for induction over integers
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 a != null
+ requires a.Length == 0 || a[0] == 0
+ requires forall j {:nowarn} :: 1 <= j < a.Length ==> a[j] == a[j-1]+2*j-1 // WISH: If induction was more powerful, we wouldn't need to rely on the quantifier to produce the j-1 term.
{
// 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 < 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 a != null
+ requires a.Length == 0 || a[0] == 0
+ requires forall j {:nowarn} :: 1 <= j < a.Length ==> a[j] == a[j-1]+2*j-1 // WISH: Same as above
{
// ...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 < a.Length ==> a[n] == n*n; // error reported
}
}
@@ -171,7 +171,7 @@ abstract module OpaqueTypesWithParameters { }
method DifferentTypes(a: array<P<int>>, b: array<P<bool>>)
- requires a != null && b != null;
+ requires a != null && b != null
// If P were a known type, then it would also be known that P<int> and P<bool>
// would be different types, and then the types of 'a' and 'b' would be different,
// which would imply that the following postcondition would hold.
|