From 27100d2a527445102b969f157e29c51925bf9cbb Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <vkuncak@gmail.com>
Date: Fri, 23 Oct 2009 15:10:21 +0000
Subject: [PATCH] cleaned up a bit
---
examples/contracts/bst/BSTAsSet.scala | 8 ++++++--
1 file changed, 6 insertions(+), 2 deletions(-)
diff --git a/examples/contracts/bst/BSTAsSet.scala b/examples/contracts/bst/BSTAsSet.scala
index 6185b8433..c3c402098 100644
--- a/examples/contracts/bst/BSTAsSet.scala
+++ b/examples/contracts/bst/BSTAsSet.scala
@@ -12,8 +12,10 @@ object BSTAsSet extends Application {
case Node(_,left,v,right) if (x > v) => Node(content + x,
left, v, right.add(x))
case Node(_,_,v,_) if (v == x) => this
+// this is due to limitation of pattern matching check
+ case _ => this
}
- } ensuring(result => (result.content == content + x))
+ } ensuring (_.content == content + x)
// patterns are exhaustive, disjoint and all reachable
def contains(key: Int): Boolean = {
@@ -22,8 +24,10 @@ object BSTAsSet extends Application {
case Node(_,_,v,right) if (key > v) => right.contains(key)
case Node(_,_,v, _) if (key == v) => true
case Empty(_) => false
+// this is due to limitation of pattern matching check
+ case _ => false
}
- } ensuring(res => (res == content.contains(key)))
+ } ensuring (_ == content.contains(key))
}
case class Empty(override val content : Set[Int]) extends BST(Set.empty)
--
GitLab