From ee51c07f16681ec2f485df2fb755aa8756c79c25 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Mon, 27 Jul 2015 18:19:20 +0200
Subject: [PATCH] some testcase for map not working
---
testcases/verification/map/BasicMap.scala | 17 +++++++++++++++++
1 file changed, 17 insertions(+)
create mode 100644 testcases/verification/map/BasicMap.scala
diff --git a/testcases/verification/map/BasicMap.scala b/testcases/verification/map/BasicMap.scala
new file mode 100644
index 000000000..2cb3a907e
--- /dev/null
+++ b/testcases/verification/map/BasicMap.scala
@@ -0,0 +1,17 @@
+import scala.collection.immutable.Set
+import leon.annotation._
+import leon.lang._
+
+object BasicMap {
+
+ def insert(m: Map[BigInt, BigInt], key: BigInt, value: BigInt): Map[BigInt, BigInt] = {
+ require(!m.isDefinedAt(key))
+ m + (key -> value)
+ } ensuring(res => res(key) == value)
+
+ def unionWorks(m1: Map[BigInt, BigInt], m2: Map[BigInt, BigInt], key: BigInt): Boolean = {
+ require(m1.isDefinedAt(key) || m2.isDefinedAt(key))
+ (m1 ++ m2).isDefinedAt(key)
+ }.holds
+
+}
--
GitLab