From 2bfb81bd10f969ad2834be5b6604606ad9c14dab Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Thu, 11 Mar 2010 00:27:39 +0000
Subject: Dafny:  Added stratosphere tests for datatypes--that is, it is now
 checked that every datatype has some value.

---
 Test/dafny0/Answer        |  8 ++++----
 Test/dafny0/Simple.dfy    |  3 ---
 Test/dafny0/TypeTests.dfy | 29 +++++++++++++++++++++++++++++
 3 files changed, 33 insertions(+), 7 deletions(-)

(limited to 'Test')

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 95302b05..1edbeedc 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1,6 +1,6 @@
 
 -------------------- Simple.dfy --------------------
-// synthetic program
+// Simple.dfy
 
 class MyClass<T, U> {
   var x: int;
@@ -57,8 +57,6 @@ datatype WildData {
   More(List<int>);
 }
 
-datatype Nothing { }
-
 class C {
   var w: WildData;
   var list: List<bool>;
@@ -78,7 +76,9 @@ TypeTests.dfy(5,13): Error: incorrect type of function argument 1 (expected D, g
 TypeTests.dfy(11,4): Error: incorrect type of method in-parameter 0 (expected int, got bool)
 TypeTests.dfy(12,4): Error: incorrect type of method out-parameter 0 (expected int, got C)
 TypeTests.dfy(12,4): Error: incorrect type of method out-parameter 1 (expected C, got int)
-7 resolution/type errors detected in synthetic program
+TypeTests.dfy(20,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Nothing' can be constructed
+TypeTests.dfy(23,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
+9 resolution/type errors detected in TypeTests.dfy
 
 -------------------- SmallTests.dfy --------------------
 SmallTests.dfy(30,7): Error: RHS expression must be well defined
diff --git a/Test/dafny0/Simple.dfy b/Test/dafny0/Simple.dfy
index c5599529..d8c8d91d 100644
--- a/Test/dafny0/Simple.dfy
+++ b/Test/dafny0/Simple.dfy
@@ -50,9 +50,6 @@ datatype WildData {
   More(List<int>);
 }
 
-datatype Nothing {
-}
-
 class C {
   var w: WildData;
   var list: List<bool>;
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 4cb02858..1616234e 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -16,3 +16,32 @@ class C {
 datatype D {
   A;
 }
+
+datatype Nothing {  // error: no grounding constructor
+}
+
+datatype NeverendingList {  // error: no grounding constructor
+  Cons(int, NeverendingList);
+}
+
+datatype MutuallyRecursiveDataType<T> {
+  FromANumber(int);  // this is the base case
+  Else(TheCounterpart<T>, C);
+}
+
+datatype TheCounterpart<T> {
+  TreeLike(TheCounterpart<T>, TheCounterpart<T>);
+  More(MutuallyRecursiveDataType<T>);
+}
+
+// these 'ReverseOrder_' order tests may be called white-box unit tests
+datatype ReverseOrder_MutuallyRecursiveDataType<T> {
+  FromANumber(int);  // this is the base case
+  Else(ReverseOrder_TheCounterpart<T>, C);
+}
+
+datatype ReverseOrder_TheCounterpart<T> {
+  TreeLike(ReverseOrder_TheCounterpart<T>, ReverseOrder_TheCounterpart<T>);
+  More(ReverseOrder_MutuallyRecursiveDataType<T>);
+}
+
-- 
cgit v1.2.3