From 927a76b4b1461ac549bc12f24c7bf73f610bd4e4 Mon Sep 17 00:00:00 2001 From: Unknown Date: Wed, 26 Jun 2013 17:48:12 -0700 Subject: Changed ranking function for Seq, so that it's compatible with data types. --- Test/dafny1/ExtensibleArray.dfy | 2 +- Test/dafny1/ExtensibleArrayAuto.dfy | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'Test/dafny1') 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 { 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 { method Append(t: T) ensures Contents == old(Contents) + [t]; - decreases Contents; + decreases |Contents|; { if (length == 0 || length % 256 != 0) { // there is room in "elements" -- cgit v1.2.3