add repack on hashmap

epfl-lara · Dec 9, 2024 · 2aaa7b3 · 2aaa7b3
1 parent 62c0ac8
commit 2aaa7b3
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableHashMap.scala b/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableHashMap.scala
@@ -232,6 +232,11 @@ object MutableHashMap {
 
     }.ensuring (res => valid && (if (res) map.eq(old(this).map - key) else map.eq(old(this).map)))
 
+    def repack(): Boolean = {
+      require(valid)
+      this.underlying.v.repack()
+    }.ensuring (res => res == false || map == old(this).map)
+
     @ghost
     override  def valid: Boolean = underlying.v.valid &&
       underlying.v.map.toList.forall((k, v) => noDuplicateKeys(v)) &&