diff options
| author |  rustanleino <unknown> | 2011-03-30 14:57:41 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2011-03-30 14:57:41 +0000 |
| commit | 6e93acd001f5d23c08b02c162dc2111e531f3d5d (patch) | |
| tree | 5ff62d24471a5447264d453ffef35a10f448afaf /Test/dafny1 | |
| parent | 5f953da880c83e1f3032c7ae2e76703418c498d4 (diff) | |
Dafny:
* Fixed handling of type parameters in automatic decreases clauses
* Added ACL2s Rotate example
Diffstat (limited to 'Test/dafny1')
| -rw-r--r-- | Test/dafny1/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny1/TreeDatatype.dfy | 36 |
2 files changed, 37 insertions, 1 deletions
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index f54c87fd..2fd70cc2 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -65,7 +65,7 @@ Dafny program verifier finished with 12 verified, 0 errors -------------------- TreeDatatype.dfy --------------------
-Dafny program verifier finished with 6 verified, 0 errors
+Dafny program verifier finished with 10 verified, 0 errors
-------------------- KatzManna.dfy --------------------
diff --git a/Test/dafny1/TreeDatatype.dfy b/Test/dafny1/TreeDatatype.dfy index 7fc62feb..f576850e 100644 --- a/Test/dafny1/TreeDatatype.dfy +++ b/Test/dafny1/TreeDatatype.dfy @@ -64,3 +64,39 @@ static function XForestInc(forest: TreeList): TreeList case Nil => forest
case Cons(tree, tail) => #TreeList.Cons(XInc(tree), XForestInc(tail))
}
+
+// ------------------ fun with recursive functions
+
+function len<T>(l: List<T>): int
+{
+ match l
+ case Nil => 0
+ case Cons(h,t) => 1 + len(t)
+}
+
+function SingletonList<T>(h: T): List<T>
+ ensures len(SingletonList(h)) == 1;
+{
+ #List.Cons(h, #List.Nil)
+}
+
+function Append<T>(a: List<T>, b: List<T>): List<T>
+ ensures len(Append(a,b)) == len(a) + len(b);
+{
+ match a
+ case Nil => b
+ case Cons(h,t) => #List.Cons(h, Append(t, b))
+}
+
+function Rotate<T>(n: int, l: List<T>): List<T>
+ requires 0 <= n;
+ ensures len(Rotate(n, l)) == len(l);
+{
+ match l
+ case Nil => l
+ case Cons(h, t) =>
+ if n == 0 then l else
+ Rotate(n-1, Append(t, SingletonList(h)))
+}
+
+
|