diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-04-27 13:30:28 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-04-27 13:30:28 -0700 |
| commit | a8bdd2aa3fcbff708b233ee321b13a17f232ce19 (patch) | |
| tree | e58e60ba287a06120df947269220a122455e6402 | |
| parent | e065edad49e5690522fa83a65c88b52cad0a3970 (diff) | |
Dafny: added resolution tests cases for inductive datatypes
| -rw-r--r-- | Test/dafny0/Answer | 5 | ||||
| -rw-r--r-- | Test/dafny0/Coinductive.dfy | 10 |
2 files changed, 13 insertions, 2 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index ed69d5db..762bdea8 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1266,8 +1266,9 @@ Dafny program verifier finished with 32 verified, 6 errors -------------------- Coinductive.dfy --------------------
Coinductive.dfy(10,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Rec_Forever' can be constructed
Coinductive.dfy(13,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
-Coinductive.dfy(51,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NotFiniteEnough_Dt' can be constructed
-3 resolution/type errors detected in Coinductive.dfy
+Coinductive.dfy(35,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'K' can be constructed
+Coinductive.dfy(61,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NotFiniteEnough_Dt' can be constructed
+4 resolution/type errors detected in Coinductive.dfy
-------------------- TypeAntecedents.dfy --------------------
TypeAntecedents.dfy(32,13): Error: assertion violation
diff --git a/Test/dafny0/Coinductive.dfy b/Test/dafny0/Coinductive.dfy index fdb8c06b..35f17c1c 100644 --- a/Test/dafny0/Coinductive.dfy +++ b/Test/dafny0/Coinductive.dfy @@ -26,6 +26,16 @@ module TestInductiveDatatypes datatype List<T> = Nil | Cons(T, List);
}
+module MoreInductive {
+ datatype Tree<G> = Node(G, List<Tree<G>>);
+ datatype List<T> = Nil | Cons(T, List<T>);
+
+ datatype M = All(List<M>);
+ datatype H<'a> = HH('a, Tree<'a>);
+ datatype K<'a> = KK('a, Tree<K<'a>>); // error
+ datatype L<'a> = LL('a, Tree<List<L<'a>>>);
+}
+
// --------------------------------------------------
module TestCoinductiveDatatypes
|