Changed ranking function for Seq, so that it's compatible with data types.

7 files changed, 140 insertions, 3 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index dd5e620f..97097cfd 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1671,6 +1671,30 @@ Execution trace:
 

 Dafny program verifier finished with 38 verified, 11 errors

 

+-------------------- RankPos.dfy --------------------

+

+Dafny program verifier finished with 11 verified, 0 errors

+

+-------------------- RankNeg.dfy --------------------

+RankNeg.dfy(7,26): Error: cannot prove termination; try supplying a decreases clause

+Execution trace:

+    (0,0): anon5_Else

+    (0,0): anon6_Then

+RankNeg.dfy(12,28): Error: cannot prove termination; try supplying a decreases clause

+Execution trace:

+    (0,0): anon5_Else

+    (0,0): anon6_Then

+RankNeg.dfy(19,31): Error: cannot prove termination; try supplying a decreases clause

+Execution trace:

+    (0,0): anon5_Else

+    (0,0): anon6_Then

+RankNeg.dfy(29,25): Error: cannot prove termination; try supplying a decreases clause

+Execution trace:

+    (0,0): anon5_Else

+    (0,0): anon6_Then

+

+Dafny program verifier finished with 1 verified, 4 errors

+

 -------------------- Superposition.dfy --------------------

 
 Verifying CheckWellformed$$_0_M0.C.M ...

diff --git a/Test/dafny0/RankNeg.dfy b/Test/dafny0/RankNeg.dfy
new file mode 100644
index 00000000..39e7630d
--- /dev/null
+++ b/Test/dafny0/RankNeg.dfy
@@ -0,0 +1,31 @@
+// Negative tests

+

+// Not well-founded mutual recursions.

+

+function seq_loop_i(xs: seq<int>): int

+{

+  if (xs == [1, 2]) then seq_loop_s([[1,2]])

+  else 0

+}

+function seq_loop_s(xs: seq<seq<int>>): int

+{

+  if (xs == [[1, 2]]) then seq_loop_i([1,2])

+  else 0

+}

+

+datatype wrap = X | WS(ds: seq<wrap>);

+function wrap_loop_1(xs: seq<wrap>): int

+{

+  if (xs == [WS([X,X])]) then wrap_loop_2(WS([X,X]))

+  else 0

+}

+function wrap_loop_2(xs: wrap): int

+{

+  if (xs == WS([X,X])) then wrap_loop_3([X,X])

+  else 0

+}

+function wrap_loop_3(xs: seq<wrap>): int

+{

+  if (xs == [X,X]) then wrap_loop_1([WS([X,X])])

+  else 0

+}

diff --git a/Test/dafny0/RankPos.dfy b/Test/dafny0/RankPos.dfy
new file mode 100644
index 00000000..bc48a6c8
--- /dev/null
+++ b/Test/dafny0/RankPos.dfy
@@ -0,0 +1,79 @@
+datatype list<A> = Nil | Cons(head: A, tail: list<A>);

+datatype d = A | B(ds: list<d>);

+datatype d2 = A2 | B2(ds: seq<d2>);

+datatype d3 = A3 | B3(ds: set<d3>);

+

+function d_size(x: d): int

+{

+  match x

+  case A => 1

+  case B(ds) => 1+ds_size(ds)

+}

+

+function ds_size(xs: list<d>): int

+{

+  match xs

+  case Nil => 1

+  case Cons(head, tail) => d_size(head)+ds_size(tail)

+}

+

+function d2_size(x: d2): int

+{

+  match x

+  case A2 => 1

+  case B2(ds) => 1+ds2_size(ds)

+}

+

+function ds2_size(xs: seq<d2>): int

+{

+  if (|xs|==0) then 1 else 1+d2_size(xs[0])+ds2_size(xs[1..])

+}

+

+function seq_dec_drop(xs: seq<int>): int

+{

+  if (|xs|==0) then 0 else

+  1+seq_dec_drop(xs[1..])

+}

+

+function seq_dec_take(xs: seq<int>): int

+{

+  if (|xs|==0) then 0 else

+  1+seq_dec_take(xs[..|xs|-1])

+}

+

+function seq_dec(xs: seq<int>): int

+{

+  if (|xs|==0) then 0 else

+  var i :| 0 < i <= |xs|;

+  i+seq_dec(xs[i..])

+}

+

+function seq_dec'(xs: seq<int>): int

+{

+  if (|xs|==0) then 0 else

+  var i :| 0 <= i < |xs|;

+  i+seq_dec'(xs[..i])

+}

+

+function seq_dec''(xs: seq<int>): int

+{

+  if (|xs|==0) then 0 else

+  var i :| 0 <= i < |xs|;

+  assert xs[0..i] == xs[..i];

+  i+seq_dec''(xs[0..i])

+}

+

+function seq_dec'''(xs: seq<int>): int

+  decreases |xs|;

+{

+  if (|xs|==0) then 0 else

+  var i :| 0 <= i < |xs|;

+  i+seq_dec'''(xs[..i]+xs[i+1..])

+}

+

+function seq_dec''''(xs: seq<int>): int

+{

+  if (|xs|==0) then 0 else

+  var i :| 0 <= i < |xs|;

+  i+seq_dec''''(xs[..i]+xs[i+1..])

+}
\ No newline at end of file
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 1bb2ef9f..c238b1f4 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -25,7 +25,8 @@ for %%f in (TypeTests.dfy NatTypes.dfy Definedness.dfy
             CallStmtTests.dfy MultiSets.dfy PredExpr.dfy

             Predicates.dfy Skeletons.dfy Maps.dfy LiberalEquality.dfy

             RefinementModificationChecking.dfy TailCalls.dfy

-            Calculations.dfy IteratorResolution.dfy Iterators.dfy) do (

+            Calculations.dfy IteratorResolution.dfy Iterators.dfy

+            RankPos.dfy RankNeg.dfy) do (

   echo.

   echo -------------------- %%f --------------------

   %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f

diff --git a/Test/dafny1/ExtensibleArray.dfy b/Test/dafny1/ExtensibleArray.dfy
index adf97863..57ac69c7 100644
--- a/Test/dafny1/ExtensibleArray.dfy
+++ b/Test/dafny1/ExtensibleArray.dfy
@@ -83,7 +83,7 @@ class ExtensibleArray<T> {
     modifies Repr;

     ensures Valid() && fresh(Repr - old(Repr));

     ensures Contents == old(Contents) + [t];

-    decreases Contents;

+    decreases |Contents|;

   {

     if (length == 0 || length % 256 != 0) {

       // there is room in "elements"

diff --git a/Test/dafny1/ExtensibleArrayAuto.dfy b/Test/dafny1/ExtensibleArrayAuto.dfy
index a3c5593c..b05af9f9 100644
--- a/Test/dafny1/ExtensibleArrayAuto.dfy
+++ b/Test/dafny1/ExtensibleArrayAuto.dfy
@@ -70,7 +70,7 @@ class {:autocontracts} ExtensibleArray<T> {
 

   method Append(t: T)

     ensures Contents == old(Contents) + [t];

-    decreases Contents;

+    decreases |Contents|;

   {

     if (length == 0 || length % 256 != 0) {

       // there is room in "elements"

diff --git a/Test/vstte2012/RingBufferAuto.dfy b/Test/vstte2012/RingBufferAuto.dfy
index f51a36b2..7ce48fcc 100644
--- a/Test/vstte2012/RingBufferAuto.dfy
+++ b/Test/vstte2012/RingBufferAuto.dfy
@@ -55,6 +55,8 @@ class {:autocontracts} RingBuffer<T>
 

   method Dequeue() returns (x: T)

     requires Contents != [];

+    modifies Repr;

+    ensures Valid() && fresh(Repr - old(Repr));

     ensures x == old(Contents)[0] && Contents == old(Contents)[1..] && N == old(N);

   {

     x := data[start];