fix: Drop SelectOpt from MutableMap (#162)

* fix: Drop SelectOpt from MutableMap * fix: MutableMap drop SelectOpt * fix: MutableMap.java * fix: MutableMap.java --------- Co-authored-by: Shubham Chaturvedi <[email protected]>
dafny-lang · Nov 14, 2024 · 4b8201a · 4b8201a
1 parent fabf44d
commit 4b8201a
Show file tree

Hide file tree

Showing 3 changed files with 1 addition and 15 deletions.
diff --git a/examples/MutableMap/MutableMapExamples.dfy b/examples/MutableMap/MutableMapExamples.dfy
@@ -57,8 +57,6 @@ module {:options "-functionSyntax:4"} MutableMapExamples {
     print m.Select("testkey2"), "\n";
 
     m.Remove("testkey");
-    AssertAndExpect(m.SelectOpt("testkey").None?);
-    AssertAndExpect(m.SelectOpt("testkey2").Some? && m.SelectOpt("testkey2").value == "testvalue2");
     AssertAndExpect(m.Keys() == {"testkey2"});
     AssertAndExpect(m.Values() == {"testvalue2"});
     AssertAndExpect(m.Items() == {("testkey2", "testvalue2")});

diff --git a/src/MutableMap/MutableMap.dfy b/src/MutableMap/MutableMap.dfy
@@ -97,17 +97,6 @@ module {:extern "DafnyLibraries"} {:options "-functionSyntax:4"} DafnyLibraries
       ensures v in this.content().Values
       ensures this.content()[k] == v
 
-    function SelectOpt(k: K): (o: Option<V>)
-      reads this
-      ensures o.Some? ==> (this.HasKey(k) && o.value in this.content().Values && this.content()[k] == o.value)
-      ensures o.None? ==> !this.HasKey(k)
-    {
-      if this.HasKey(k) then
-        Some(this.Select(k))
-      else
-        None
-    }
-
     method {:extern} Remove(k: K)
       modifies this
       ensures this.content() == old(this.content()) - {k}

diff --git a/src/MutableMap/MutableMap.java b/src/MutableMap/MutableMap.java
@@ -15,11 +15,10 @@
 import java.util.Map;
 import java.math.BigInteger;
 
-public class MutableMap<K,V> extends _ExternBase_MutableMap<K,V> {
+public class MutableMap<K, V> implements DafnyLibraries.MutableMapTrait<K, V> {
   private ConcurrentHashMap<K,V> m;
 
   public MutableMap(dafny.TypeDescriptor<K> _td_K, dafny.TypeDescriptor<V> _td_V) {
-    super(_td_K, _td_V);
     m = new ConcurrentHashMap<K,V>();
   }