diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-10-16 18:09:13 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-10-16 18:09:13 -0700 |
| commit | 6044f08dceb6c03e7b6e8924186a301dcc2e7e97 (patch) | |
| tree | a30712837253fbec39e46f226e24ed73afa0b4ca /Test/dafny0/Termination.dfy | |
| parent | e889485e915a28aa499d19bc194bc731c89033b9 (diff) | |
Added/fixed decreases clauses that use multisets or maps.
Diffstat (limited to 'Test/dafny0/Termination.dfy')
| -rw-r--r-- | Test/dafny0/Termination.dfy | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy index bc431450..83baade1 100644 --- a/Test/dafny0/Termination.dfy +++ b/Test/dafny0/Termination.dfy @@ -372,3 +372,41 @@ class DefaultDecreasesFunction { if x < 0 then -x else x
}
}
+
+// ----------------- multisets and maps ----------
+
+module MultisetTests {
+ function F(a: multiset<int>, n: nat): int
+ decreases a, n;
+ {
+ if n == 0 then 0 else F(a, n-1)
+ }
+
+ function F'(a: multiset<int>, n: nat): int // inferred decreases clause
+ {
+ if n == 0 then 0 else F'(a, n-1)
+ }
+
+ ghost method M(n: nat, b: multiset<int>)
+ ensures F(b, n) == 0; // proved via automatic induction
+ {
+ }
+}
+
+module MapTests {
+ function F(a: map<int,int>, n: nat): int
+ decreases a, n;
+ {
+ if n == 0 then 0 else F(a, n-1)
+ }
+
+ function F'(a: map<int,int>, n: nat): int // inferred decreases clause
+ {
+ if n == 0 then 0 else F'(a, n-1)
+ }
+
+ ghost method M(n: nat, b: map<int,int>)
+ ensures F(b, n) == 0; // proved via automatic induction
+ {
+ }
+}
|