From 607ef28aadb281ab61a2be493a637126e967a388 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Thu, 29 May 2014 21:41:00 +0200 Subject: Set up the same test infrastructure as in Boogie. --- Test/VSComp2010/Problem1-SumMax.dfy | 3 +++ Test/VSComp2010/Problem1-SumMax.dfy.expect | 2 ++ Test/VSComp2010/Problem2-Invert.dfy | 3 +++ Test/VSComp2010/Problem2-Invert.dfy.expect | 2 ++ Test/VSComp2010/Problem3-FindZero.dfy | 3 +++ Test/VSComp2010/Problem3-FindZero.dfy.expect | 2 ++ Test/VSComp2010/Problem4-Queens.dfy | 3 +++ Test/VSComp2010/Problem4-Queens.dfy.expect | 2 ++ Test/VSComp2010/Problem5-DoubleEndedQueue.dfy | 3 +++ Test/VSComp2010/Problem5-DoubleEndedQueue.dfy.expect | 2 ++ 10 files changed, 25 insertions(+) create mode 100644 Test/VSComp2010/Problem1-SumMax.dfy.expect create mode 100644 Test/VSComp2010/Problem2-Invert.dfy.expect create mode 100644 Test/VSComp2010/Problem3-FindZero.dfy.expect create mode 100644 Test/VSComp2010/Problem4-Queens.dfy.expect create mode 100644 Test/VSComp2010/Problem5-DoubleEndedQueue.dfy.expect (limited to 'Test/VSComp2010') diff --git a/Test/VSComp2010/Problem1-SumMax.dfy b/Test/VSComp2010/Problem1-SumMax.dfy index 3db9bf72..d7989539 100644 --- a/Test/VSComp2010/Problem1-SumMax.dfy +++ b/Test/VSComp2010/Problem1-SumMax.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + // VSComp 2010, problem 1, compute the sum and max of the elements of an array and prove // that 'sum <= N * max'. // Rustan Leino, 18 August 2010. diff --git a/Test/VSComp2010/Problem1-SumMax.dfy.expect b/Test/VSComp2010/Problem1-SumMax.dfy.expect new file mode 100644 index 00000000..73ba063c --- /dev/null +++ b/Test/VSComp2010/Problem1-SumMax.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 4 verified, 0 errors diff --git a/Test/VSComp2010/Problem2-Invert.dfy b/Test/VSComp2010/Problem2-Invert.dfy index 327703e7..23c25733 100644 --- a/Test/VSComp2010/Problem2-Invert.dfy +++ b/Test/VSComp2010/Problem2-Invert.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + // VSComp 2010, problem 2, compute the inverse 'B' of a permutation 'A' and prove that 'B' is // indeed an inverse of 'A' (or at least prove that 'B' is injective). // Rustan Leino, 31 August 2010. diff --git a/Test/VSComp2010/Problem2-Invert.dfy.expect b/Test/VSComp2010/Problem2-Invert.dfy.expect new file mode 100644 index 00000000..76f19e0d --- /dev/null +++ b/Test/VSComp2010/Problem2-Invert.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 7 verified, 0 errors diff --git a/Test/VSComp2010/Problem3-FindZero.dfy b/Test/VSComp2010/Problem3-FindZero.dfy index 3d24255d..61bb2e3a 100644 --- a/Test/VSComp2010/Problem3-FindZero.dfy +++ b/Test/VSComp2010/Problem3-FindZero.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + // VSComp 2010, problem 3, find a 0 in a linked list and return how many nodes were skipped // until the first 0 (or end-of-list) was found. // Rustan Leino, 18 August 2010. diff --git a/Test/VSComp2010/Problem3-FindZero.dfy.expect b/Test/VSComp2010/Problem3-FindZero.dfy.expect new file mode 100644 index 00000000..76f19e0d --- /dev/null +++ b/Test/VSComp2010/Problem3-FindZero.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 7 verified, 0 errors diff --git a/Test/VSComp2010/Problem4-Queens.dfy b/Test/VSComp2010/Problem4-Queens.dfy index 2d4111db..21fcc053 100644 --- a/Test/VSComp2010/Problem4-Queens.dfy +++ b/Test/VSComp2010/Problem4-Queens.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + // VSComp 2010, problem 4, N queens // Rustan Leino, 31 August 2010, updated 24 March 2011. // diff --git a/Test/VSComp2010/Problem4-Queens.dfy.expect b/Test/VSComp2010/Problem4-Queens.dfy.expect new file mode 100644 index 00000000..249e77e5 --- /dev/null +++ b/Test/VSComp2010/Problem4-Queens.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 9 verified, 0 errors diff --git a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy index 0e141927..930758a5 100644 --- a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy +++ b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + // VSComp 2010, problem 5, double-ended queue. // Rustan Leino, 18 August 2010. // diff --git a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy.expect b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy.expect new file mode 100644 index 00000000..73727958 --- /dev/null +++ b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 21 verified, 0 errors -- cgit v1.2.3