diff options
| author |  rustanleino <unknown> | 2010-06-08 18:05:23 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-06-08 18:05:23 +0000 |
| commit | 2e8f477b81b1c5c6d3c3f600abac3874548a9e4d (patch) | |
| tree | 03e89bdb4df3a689b7217c5e913557c5b6c6df99 /Test/dafny1/TerminationDemos.dfy | |
| parent | 22e67dc18705c19b617678358c8e859349938ac3 (diff) | |
Boogie:
* Look for Z3 versions up to 2.15 (but did not implement a better algorithm for it).
* Added prover-path output as part of /trace flag (that probably isn't the best command-line option for it).
Dafny:
* Split off some tests from Test/dafny0 into Test/dafny1.
* Added Test/dafny1/UltraFilter.dfy.
Diffstat (limited to 'Test/dafny1/TerminationDemos.dfy')
| -rw-r--r-- | Test/dafny1/TerminationDemos.dfy | 80 |
1 files changed, 80 insertions, 0 deletions
diff --git a/Test/dafny1/TerminationDemos.dfy b/Test/dafny1/TerminationDemos.dfy new file mode 100644 index 00000000..6b63bfec --- /dev/null +++ b/Test/dafny1/TerminationDemos.dfy @@ -0,0 +1,80 @@ +class Example {
+ method M(n: int)
+ {
+ var i := 0;
+ while (i < n)
+ decreases n - i;
+ {
+ i := i + 1;
+ }
+ }
+}
+
+// -----------------------------------
+
+class Fibonacci {
+ function Fib(n: int): int
+ decreases n;
+ {
+ if n < 2 then n else Fib(n-2) + Fib(n-1)
+ }
+}
+
+// -----------------------------------
+
+class Ackermann {
+ function F(m: int, n: int): int
+ decreases m, n;
+ {
+ if m <= 0 then
+ n + 1
+ else if n <= 0 then
+ F(m - 1, 1)
+ else
+ F(m - 1, F(m, n - 1))
+ }
+}
+
+// -----------------------------------
+
+class List {
+ var data: int;
+ var next: List;
+ ghost var ListNodes: set<List>;
+ function IsAcyclic(): bool
+ reads *;
+ decreases ListNodes;
+ {
+ this in ListNodes &&
+ (next != null ==>
+ next.ListNodes <= ListNodes && this !in next.ListNodes &&
+ next.IsAcyclic())
+ }
+
+ method Singleton(x: int) returns (list: List)
+ ensures list != null && list.IsAcyclic();
+ {
+ list := new List;
+ list.data := x;
+ list.next := null;
+ list.ListNodes := {list};
+ }
+
+ method Prepend(x: int, tail: List) returns (list: List)
+ requires tail == null || tail.IsAcyclic();
+ ensures list != null && list.IsAcyclic();
+ {
+ list := new List;
+ list.data := x;
+ list.next := tail;
+ list.ListNodes := if tail == null then {list} else {list} + tail.ListNodes;
+ }
+
+ function Sum(): int
+ requires IsAcyclic();
+ reads *;
+ decreases ListNodes;
+ {
+ if next == null then data else data + next.Sum()
+ }
+}
|