Dafny: Added stratosphere tests for datatypes--that is, it is now checked that every datatype has some value.

3 files changed, 33 insertions, 7 deletions

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>);

+}

+