Set up the same test infrastructure as in Boogie.

32 files changed, 80 insertions, 0 deletions

diff --git a/Test/dafny3/CachedContainer.dfy b/Test/dafny3/CachedContainer.dfy
index 6ac5ff2f..18c12862 100644
--- a/Test/dafny3/CachedContainer.dfy
+++ b/Test/dafny3/CachedContainer.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 // give the method signatures and specs

 abstract module M0 {

   class {:autocontracts} Container<T(==)> {

diff --git a/Test/dafny3/CachedContainer.dfy.expect b/Test/dafny3/CachedContainer.dfy.expect
new file mode 100644
index 00000000..c6c90498
--- /dev/null
+++ b/Test/dafny3/CachedContainer.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 47 verified, 0 errors

diff --git a/Test/dafny3/CalcExample.dfy b/Test/dafny3/CalcExample.dfy
index dcd41077..2782d049 100644
--- a/Test/dafny3/CalcExample.dfy
+++ b/Test/dafny3/CalcExample.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 function f(x: int, y: int): int

 

 ghost method Associativity(x: int, y: int, z: int)

diff --git a/Test/dafny3/CalcExample.dfy.expect b/Test/dafny3/CalcExample.dfy.expect
new file mode 100644
index 00000000..4ef2de53
--- /dev/null
+++ b/Test/dafny3/CalcExample.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 6 verified, 0 errors

diff --git a/Test/dafny3/Dijkstra.dfy b/Test/dafny3/Dijkstra.dfy
index ef94f291..e90687e0 100644
--- a/Test/dafny3/Dijkstra.dfy
+++ b/Test/dafny3/Dijkstra.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 // Example taken from:

 // Edsger W. Dijkstra: Heuristics for a Calculational Proof. Inf. Process. Lett. (IPL) 53(3):141-143 (1995)

 // Transcribed into Dafny by Valentin Wüstholz and Nadia Polikarpova.

diff --git a/Test/dafny3/Dijkstra.dfy.expect b/Test/dafny3/Dijkstra.dfy.expect
new file mode 100644
index 00000000..b9a9bc89
--- /dev/null
+++ b/Test/dafny3/Dijkstra.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 12 verified, 0 errors

diff --git a/Test/dafny3/Filter.dfy b/Test/dafny3/Filter.dfy
index 4b39876a..0d9a7231 100644
--- a/Test/dafny3/Filter.dfy
+++ b/Test/dafny3/Filter.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 codatatype Stream<T> = Cons(head: T, tail: Stream);

 

 function Tail(s: Stream, n: nat): Stream

diff --git a/Test/dafny3/Filter.dfy.expect b/Test/dafny3/Filter.dfy.expect
new file mode 100644
index 00000000..91aa9b47
--- /dev/null
+++ b/Test/dafny3/Filter.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 43 verified, 0 errors

diff --git a/Test/dafny3/GenericSort.dfy b/Test/dafny3/GenericSort.dfy
index 10589e5a..53d98bc2 100644
--- a/Test/dafny3/GenericSort.dfy
+++ b/Test/dafny3/GenericSort.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 abstract module TotalOrder {

   type T // the type to be compared

   static predicate method Leq(a: T, b: T) // Leq(a,b) iff a <= b

diff --git a/Test/dafny3/GenericSort.dfy.expect b/Test/dafny3/GenericSort.dfy.expect
new file mode 100644
index 00000000..f5e3b3dc
--- /dev/null
+++ b/Test/dafny3/GenericSort.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 36 verified, 0 errors

diff --git a/Test/dafny3/InductionVsCoinduction.dfy b/Test/dafny3/InductionVsCoinduction.dfy
index 5c5c0412..47754036 100644
--- a/Test/dafny3/InductionVsCoinduction.dfy
+++ b/Test/dafny3/InductionVsCoinduction.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 // A definition of a co-inductive datatype Stream, whose values are possibly

 // infinite lists.

 codatatype Stream<T> = SNil | SCons(head: T, tail: Stream<T>);

diff --git a/Test/dafny3/InductionVsCoinduction.dfy.expect b/Test/dafny3/InductionVsCoinduction.dfy.expect
new file mode 100644
index 00000000..c192e07c
--- /dev/null
+++ b/Test/dafny3/InductionVsCoinduction.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 20 verified, 0 errors

diff --git a/Test/dafny3/InfiniteTrees.dfy b/Test/dafny3/InfiniteTrees.dfy
index 32a868bb..030443c0 100644
--- a/Test/dafny3/InfiniteTrees.dfy
+++ b/Test/dafny3/InfiniteTrees.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 // Here is the usual definition of possibly infinite lists, along with a function Tail(s, n), which drops

 // n heads from s, and two lemmas that prove properties of Tail.

 

diff --git a/Test/dafny3/InfiniteTrees.dfy.expect b/Test/dafny3/InfiniteTrees.dfy.expect
new file mode 100644
index 00000000..79f8263d
--- /dev/null
+++ b/Test/dafny3/InfiniteTrees.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 88 verified, 0 errors

diff --git a/Test/dafny3/Iter.dfy b/Test/dafny3/Iter.dfy
index c5e8f3a3..5ada6f5b 100644
--- a/Test/dafny3/Iter.dfy
+++ b/Test/dafny3/Iter.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 class List<T> {

   ghost var Contents: seq<T>;

   ghost var Repr: set<object>;

diff --git a/Test/dafny3/Iter.dfy.expect b/Test/dafny3/Iter.dfy.expect
new file mode 100644
index 00000000..b06ff8fc
--- /dev/null
+++ b/Test/dafny3/Iter.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 15 verified, 0 errors

diff --git a/Test/dafny3/OpaqueTrees.dfy b/Test/dafny3/OpaqueTrees.dfy
index a08d0b68..53540c1d 100644
--- a/Test/dafny3/OpaqueTrees.dfy
+++ b/Test/dafny3/OpaqueTrees.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 datatype Tree<T> = Leaf(T) | Node(Tree, Tree)

 

 function {:opaque} size(t: Tree): nat

diff --git a/Test/dafny3/OpaqueTrees.dfy.expect b/Test/dafny3/OpaqueTrees.dfy.expect
new file mode 100644
index 00000000..4ef2de53
--- /dev/null
+++ b/Test/dafny3/OpaqueTrees.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 6 verified, 0 errors

diff --git a/Test/dafny3/Paulson.dfy b/Test/dafny3/Paulson.dfy
index 37586ec7..735963a5 100644
--- a/Test/dafny3/Paulson.dfy
+++ b/Test/dafny3/Paulson.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 // The following are Dafny versions from Section 8 of

 // "Mechanizing Coinduction and Corecursion in Higher-order Logic"

 // by Lawrence C. Paulson, 1996.

diff --git a/Test/dafny3/Paulson.dfy.expect b/Test/dafny3/Paulson.dfy.expect
new file mode 100644
index 00000000..ab18d98e
--- /dev/null
+++ b/Test/dafny3/Paulson.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 28 verified, 0 errors

diff --git a/Test/dafny3/SetIterations.dfy b/Test/dafny3/SetIterations.dfy
index 8b095b5f..2319078a 100644
--- a/Test/dafny3/SetIterations.dfy
+++ b/Test/dafny3/SetIterations.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 function Count<T>(s: set<T>): int

 {

   if s == {} then 0 else

diff --git a/Test/dafny3/SetIterations.dfy.expect b/Test/dafny3/SetIterations.dfy.expect
new file mode 100644
index 00000000..aeb37948
--- /dev/null
+++ b/Test/dafny3/SetIterations.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 13 verified, 0 errors

diff --git a/Test/dafny3/SimpleCoinduction.dfy b/Test/dafny3/SimpleCoinduction.dfy
index b5b0c8bf..5be5c569 100644
--- a/Test/dafny3/SimpleCoinduction.dfy
+++ b/Test/dafny3/SimpleCoinduction.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 codatatype Stream<T> = Cons(head: T, tail: Stream);

 codatatype IList<T> = Nil | ICons(head: T, tail: IList);

 

diff --git a/Test/dafny3/SimpleCoinduction.dfy.expect b/Test/dafny3/SimpleCoinduction.dfy.expect
new file mode 100644
index 00000000..58598e51
--- /dev/null
+++ b/Test/dafny3/SimpleCoinduction.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 31 verified, 0 errors

diff --git a/Test/dafny3/SimpleInduction.dfy b/Test/dafny3/SimpleInduction.dfy
index 700b531c..29660099 100644
--- a/Test/dafny3/SimpleInduction.dfy
+++ b/Test/dafny3/SimpleInduction.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 /*

   The well-known Fibonacci function defined in Dafny.  The postcondition of

   method FibLemma states a property about Fib, and the body of the method is

diff --git a/Test/dafny3/SimpleInduction.dfy.expect b/Test/dafny3/SimpleInduction.dfy.expect
new file mode 100644
index 00000000..b9a9bc89
--- /dev/null
+++ b/Test/dafny3/SimpleInduction.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 12 verified, 0 errors

diff --git a/Test/dafny3/Streams.dfy b/Test/dafny3/Streams.dfy
index 1d566545..c51f30d4 100644
--- a/Test/dafny3/Streams.dfy
+++ b/Test/dafny3/Streams.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 // ----- Stream

 

 codatatype Stream<T> = Nil | Cons(head: T, tail: Stream);

diff --git a/Test/dafny3/Streams.dfy.expect b/Test/dafny3/Streams.dfy.expect
new file mode 100644
index 00000000..c90560b0
--- /dev/null
+++ b/Test/dafny3/Streams.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 52 verified, 0 errors

diff --git a/Test/dafny3/WideTrees.dfy b/Test/dafny3/WideTrees.dfy
index 3fa99256..0245ef9f 100644
--- a/Test/dafny3/WideTrees.dfy
+++ b/Test/dafny3/WideTrees.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 codatatype Stream<T> = SNil | SCons(head: T, tail: Stream)

 datatype Tree = Node(children: Stream<Tree>)

 

diff --git a/Test/dafny3/WideTrees.dfy.expect b/Test/dafny3/WideTrees.dfy.expect
new file mode 100644
index 00000000..c87e2af2
--- /dev/null
+++ b/Test/dafny3/WideTrees.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 10 verified, 0 errors

diff --git a/Test/dafny3/Zip.dfy b/Test/dafny3/Zip.dfy
index 629861f9..9b1d3671 100644
--- a/Test/dafny3/Zip.dfy
+++ b/Test/dafny3/Zip.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 /*

 Here, we define infinite streams with some functions and prove a few

 properties, drawing from:

diff --git a/Test/dafny3/Zip.dfy.expect b/Test/dafny3/Zip.dfy.expect
new file mode 100644
index 00000000..acae4413
--- /dev/null
+++ b/Test/dafny3/Zip.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 24 verified, 0 errors