diff options
Diffstat (limited to 'Test/dafny0/DTypes.dfy')
| -rw-r--r-- | Test/dafny0/DTypes.dfy | 156 |
1 files changed, 0 insertions, 156 deletions
diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy deleted file mode 100644 index 55d107c5..00000000 --- a/Test/dafny0/DTypes.dfy +++ /dev/null @@ -1,156 +0,0 @@ -class C {
- var n: set<Node>;
-
- method M(v: Stack)
- requires v != null;
- {
- var o: object := v;
- assert o !in n; // should be known from the types involved
- }
-
- method N(v: Stack)
- /* this time without the precondition */
- {
- var o: object := v;
- assert o !in n; // error: v may be null
- }
-
- method A0(a: CP<int,C>, b: CP<int,object>)
- {
- var x: object := a;
- var y: object := b;
- assert x == y ==> x == null;
- }
-
- method A1(a: CP<int,C>)
- {
- var x: object := a;
- assert (forall b: CP<int,Stack> :: 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;
- {
- var x: set<object> := a2x;
- var y: set<object> := b;
- assert x * y == {};
- }
-
- method A3(b: set<CP<Node,C>>)
- /* this time without the precondition */
- {
- var x: set<object> := a2x;
- var y: set<object> := b;
- assert x * y <= {null};
- }
-
- method A4(b: set<CP<Node,C>>)
- /* again, without the precondition */
- {
- var x: set<object> := a2x;
- var y: set<object> := b;
- assert x * y == {}; // error
- }
-
- method A5()
- {
- var a := new CP<int,C>;
- var b := new CP<int,object>;
- while (a != null)
- decreases *; // omit loop termination check (in fact, the loop does not terminate)
- {
- var x: object := a;
- var y: object := b;
- assert x == y ==> x == null;
- a := a; // make 'a' a loop target
- }
- }
-}
-
-class Stack { }
-class Node { }
-
-class CP<T,U> {
-}
-
-datatype Data = Lemon | Kiwi(int);
-
-function G(d: Data): int
- requires d != Data.Lemon;
-{
- match d
- case Lemon => G(d)
- case Kiwi(x) => 7
-}
-
-// -------- some things about induction ---------------------------------
-
-datatype Tree<T> = Leaf(T) | Branch(Tree<T>, Tree<T>);
-
-class DatatypeInduction<T> {
- function LeafCount<G>(tree: Tree<G>): int
- {
- match tree
- case Leaf(t) => 1
- case Branch(left, right) => LeafCount(left) + LeafCount(right)
- }
-
- method Theorem0(tree: Tree<T>)
- 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);
- {
- 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;
- {
- assert (forall t: Tree<T> :: LeafCount(t) % 2 == 1); // error: fails for Branch case
- }
-
- method NotATheorem1(tree: Tree<T>)
- ensures 2 <= LeafCount(tree);
- {
- assert (forall t: Tree<T> :: 2 <= LeafCount(t)); // error: fails for Leaf case
- }
-
- function Predicate(): bool
- {
- (forall t: Tree<T> :: 2 <= LeafCount(t))
- }
-
- method NotATheorem2()
- {
- assert Predicate(); // error (this tests Related Location for induction via a predicate)
- }
-
- // ----- 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;
- {
- // The following assertion can be proved by induction:
- 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;
- {
- // ...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
- }
-}
|