diff options
| author |  Unknown <namin@idea> | 2013-06-26 17:48:12 -0700 |
|---|---|---|
| committer | Unknown <namin@idea> | 2013-06-26 17:48:12 -0700 |
| commit | 927a76b4b1461ac549bc12f24c7bf73f610bd4e4 (patch) | |
| tree | f92d6c14e6d0ad1e17401a8dd1a822530d37eab2 /Test/dafny1 | |
| parent | 23ad17c104cc8814c2b94a608386c0535f6d0f2f (diff) | |
Changed ranking function for Seq, so that it's compatible with data types.
Diffstat (limited to 'Test/dafny1')
| -rw-r--r-- | Test/dafny1/ExtensibleArray.dfy | 2 | ||||
| -rw-r--r-- | Test/dafny1/ExtensibleArrayAuto.dfy | 2 |
2 files changed, 2 insertions, 2 deletions
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"
|