From c2f832d15691a0fa956b5c94bb3f1e1759476932 Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <vkuncak@gmail.com>
Date: Fri, 16 Jul 2010 15:08:42 +0000
Subject: [PATCH] more examples and a bug
---
testcases/MultiBug.scala | 10 ++++++++++
testcases/MultiExample.scala | 20 ++++++++++++++++++++
2 files changed, 30 insertions(+)
create mode 100644 testcases/MultiBug.scala
create mode 100644 testcases/MultiExample.scala
diff --git a/testcases/MultiBug.scala b/testcases/MultiBug.scala
new file mode 100644
index 000000000..1336fa8f5
--- /dev/null
+++ b/testcases/MultiBug.scala
@@ -0,0 +1,10 @@
+import scala.collection.immutable.Set
+import scala.collection.immutable.Multiset
+
+object MultisetOperations {
+
+ def disjointUnion2(a: Multiset[Int], b: Multiset[Int]) : Multiset[Int] = {
+ a +++ b
+ } ensuring(res => res.toSet == (a.toSet ++ b.toSet))
+
+}
diff --git a/testcases/MultiExample.scala b/testcases/MultiExample.scala
new file mode 100644
index 000000000..732cbaa08
--- /dev/null
+++ b/testcases/MultiExample.scala
@@ -0,0 +1,20 @@
+import scala.collection.immutable.Set
+import scala.collection.immutable.Multiset
+
+object MultisetOperations {
+
+/*
+ def disjointUnion1(a: Multiset[Int], b: Multiset[Int]) : Multiset[Int] = {
+ a +++ b
+ } ensuring(res => res.size == a.size + b.size)
+
+ def preservedUnderToSet1(a: Multiset[Int], b: Multiset[Int]) : Multiset[Int] = {
+ a ++ b
+ } ensuring(res => res.toSet == a.toSet ++ b.toSet)
+
+ def preservedUnderToSet2(a: Multiset[Int], b: Multiset[Int]) : Multiset[Int] = {
+ a ** b
+ } ensuring(res => res.toSet == a.toSet ** b.toSet)
+*/
+
+}
--
GitLab