diff --git a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/ListMap.scala b/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/ListMap.scala index 34515fe6..1d4392d1 100644 --- a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/ListMap.scala +++ b/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/ListMap.scala @@ -97,9 +97,10 @@ case class ListMap[K, B](toList: List[(K, B)]) { ListMap(newList) }.ensuring(res => - res.contains(keyValue._1) && res.get(keyValue._1) == Some[B]( - keyValue._2 - ) && res.toList.contains(keyValue) + res.contains(keyValue._1) + && res.get(keyValue._1) == Some[B](keyValue._2) + && res.toList.contains(keyValue) + && res.keys().content == this.keys().content ++ Set(keyValue._1) ) def ++(keyValues: List[(K, B)]): ListMap[K, B] = { @@ -406,19 +407,6 @@ object TupleListOpsGenK { case Nil() => () } }.ensuring(_ => getKeysList(l).content - key == getKeysList(removePresrvNoDuplicatedKeys(l, key)).content) - - @opaque - @inlineOnce - def lemmaEqMapSameKeysSet[K, B](lm1: ListMap[K, B], lm2: ListMap[K, B]): Unit = { - require(lm1.eq(lm2)) - assert(lm1.toList.content == lm2.toList.content) - ListSpecs.subsetRefl(lm1.toList) - ListSpecs.subsetRefl(lm2.toList) - lemmaSubsetThenKeysSubset(lm1.toList, lm2.toList) - lemmaSubsetThenKeysSubset(lm2.toList, lm1.toList) - assert(lm1.keys().content.subsetOf(lm2.keys().content)) - assert(lm2.keys().content.subsetOf(lm1.keys().content)) - }.ensuring(_ => lm1.keys().content == lm2.keys().content) @opaque @inlineOnce @@ -505,6 +493,30 @@ object TupleListOpsGenK { case Nil() => () } }.ensuring(_ => l1.forall(p)) + + @opaque + @inlineOnce + def lemmaForallSubsetKeys[K]( + l1: List[K], + l2: List[K], + p: K => Boolean + ): Unit = { + require(l2.forall(p)) + require(l1.content.subsetOf(l2.content)) + decreases(l1) + + l1 match { + case Cons(head, tl) => + ListSpecs.subsetContains(l1, l2) + ListSpecs.forallContained(l1, l2.contains , head) + ListSpecs.forallContained(l2, p, head) + assert(l2.contains(head)) + lemmaForallSubsetKeys(tl, l2, p) + assert(tl.forall(p)) + assert(p(head)) + case Nil() => () + } + }.ensuring(_ => l1.forall(p)) @opaque @inlineOnce @@ -1501,6 +1513,19 @@ object ListMapLemmas { ) // Equivalence LEMMAS ---------------------------------------------------------------------------------------------------------------- + @opaque + @inlineOnce + def lemmaEqMapSameKeysSet[K, B](lm1: ListMap[K, B], lm2: ListMap[K, B]): Unit = { + require(lm1.eq(lm2)) + assert(lm1.toList.content == lm2.toList.content) + ListSpecs.subsetRefl(lm1.toList) + ListSpecs.subsetRefl(lm2.toList) + TupleListOpsGenK.lemmaSubsetThenKeysSubset(lm1.toList, lm2.toList) + TupleListOpsGenK.lemmaSubsetThenKeysSubset(lm2.toList, lm1.toList) + assert(lm1.keys().content.subsetOf(lm2.keys().content)) + assert(lm2.keys().content.subsetOf(lm1.keys().content)) + }.ensuring(_ => lm1.keys().content == lm2.keys().content) + @opaque @inlineOnce def lemmaAddToEqMapsPreservesEq[K, B]( 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 index 4ec56b9c..073034a3 100644 --- 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 @@ -40,7 +40,8 @@ object MutableHashMap { val underlying: Cell[LongMap[List[(K, V)]]], val hashF: Hashable[K], var _size: Int, - val defaultValue: K => V + val defaultValue: K => V, + var keys: List[K] = Nil[K]() ) extends MutableMap[K, V] { @pure @@ -123,6 +124,7 @@ object MutableHashMap { require(valid) @ghost val oldMap = map @ghost val oldLongListMap = underlying.v.map + @ghost val oldKeyList = keys val contained = contains(key) val res = if (contained) { @@ -146,9 +148,28 @@ object MutableHashMap { check(underlying.v.map.toList.forall((k, v) => noDuplicateKeys(v))) check(allKeysSameHashInMap(underlying.v.map, hashF)) check(map.eq(oldMap + (key, v))) + + // this.map.keys().forall(k => keysList.contains(k)) + ListMapLemmas.lemmaEqMapSameKeysSet(oldMap + (key, v), map) + assert(this.map.keys().content == oldMap.keys().content + key) + assert(oldMap.keys().content.contains(key)) + assert(oldMap.keys().content + key == oldMap.keys().content) + assert(this.map.keys().content == oldMap.keys().content) + val keysList = this.keys + TupleListOpsGenK.lemmaForallSubsetKeys(this.map.keys(), oldMap.keys(), k => keysList.contains(k)) + assert(this.map.keys().forall(k => keysList.contains(k))) + ListSpecs.forallContained(this.map.keys(), k => keysList.contains(k), key) + + check(keys.contains(key)) + check(valid) } else { + // this.map.keys().forall(k => keysList.contains(k)) + val keysList = this.keys + ListSpecs.forallContained(this.map.keys(), k => keysList.contains(k), key) + check(keys.contains(key)) check(valid) check(map == oldMap) + check(valid) } }) if (res && !contained) then _size += 1 @@ -161,6 +182,10 @@ object MutableHashMap { val newBucket = Cons((key, v), currentBucket) val res = underlying.v.update(hash, newBucket) + if (res && !contained) then + _size += 1 + keys = Cons(key, keys) + ghostExpr({ if (res) { if (!currentBucket.isEmpty) { @@ -176,13 +201,28 @@ object MutableHashMap { ListMapLemmas.lemmaEquivalentThenSameContains(map, oldMap + (key, v), key) check((oldMap + (key, v)).contains(key)) check(map.contains(key)) + check(keys.contains(key)) + check(simpleValid) + val keysList = this.keys + ListMapLemmas.lemmaEqMapSameKeysSet(oldMap + (key, v), map) + assert(this.map.keys().content == oldMap.keys().content + key) + check(oldMap.keys().forall(k => oldKeyList.contains(k))) + ListSpecs.forallContainsSubset(oldMap.keys(), oldKeyList) + assert(oldMap.keys().content.subsetOf(oldKeyList.content)) + assert(oldKeyList.content.subsetOf(keysList.content)) + ListSpecs.subsetContains(oldMap.keys(), keysList) + check(oldMap.keys().forall(k => keysList.contains(k))) + assert(keysList.content == oldKeyList.content + key) + assert(this.map.keys().content.subsetOf(keysList.content)) + ListSpecs.subsetContains(this.map.keys(), keysList) + check(this.map.keys().forall(k => keysList.contains(k))) + check(valid) } else { check(valid) check(map == oldMap) } }) - if (res && !contained) then _size += 1 res } res @@ -218,10 +258,17 @@ object MutableHashMap { lemmaChangeOneBucketByAValidOnePreservesForallNoDuplicatesAndHash(oldLongListMap, hash, newBucket, hashF) check(underlying.v.map.toList.forall((k, v) => noDuplicateKeys(v))) check(allKeysSameHashInMap(underlying.v.map, hashF)) - check(valid) check(oldMap.contains(key)) lemmaChangeOneBucketToRemoveAKeyRemoveThisKeyInGenMap(oldLongListMap, hash, newBucket, key, hashF) check(map.eq(oldMap - key)) + ListMapLemmas.lemmaEqMapSameKeysSet(oldMap - key, map) + assert(this.map.keys().content == oldMap.keys().content - key) + val keysList = this.keys + ListSpecs.forallContainsSubset(oldMap.keys(), keysList) + assert(this.map.keys().content.subsetOf(keysList.content)) + ListSpecs.subsetContains(this.map.keys(), keysList) + + check(valid) } else { check(valid) check(map == oldMap) @@ -232,15 +279,63 @@ object MutableHashMap { }.ensuring (res => valid && (if (res) map.eq(old(this).map - key) else map.eq(old(this).map))) + override def getKeys(): List[K] = { + require(valid) + filterKeys(keys) + }.ensuring(res => valid && ListSpecs.noDuplicate(res) && res.content == map.keys().content) + + @pure + def filterKeys(l: List[K], acc: List[K] = Nil()): List[K] = { + require(valid) + require({ + val aMap = map + acc.forall(k => aMap.contains(k)) + }) + require({ + val aMap = map + map.keys().content.subsetOf(l.content ++ acc.content) + }) + decreases(l) + @ghost val aMap = map + l match { + case Cons(hd, tl) if this.contains(hd) && !acc.contains(hd) => + val res = filterKeys(tl, Cons(hd, acc)) + assert(ListSpecs.noDuplicate(res) ) + assert(res.content.subsetOf(l.content) ) + assert(res.forall(k => aMap.contains(k))) + res + case Cons(_, tl) => + val res = filterKeys(tl, acc) + assert(ListSpecs.noDuplicate(res) ) + assert(res.content.subsetOf(l.content) ) + assert(res.forall(k => aMap.contains(k))) + res + case Nil() => acc + } + + }.ensuring(res => + val aMap = map + ListSpecs.noDuplicate(res) + && res.content.subsetOf(l.content) + && res.forall(k => aMap.contains(k))) + @ghost - override def valid: Boolean = underlying.v.valid && + @inline + def simpleValid: Boolean = + underlying.v.valid && underlying.v.map.toList.forall((k, v) => noDuplicateKeys(v)) && allKeysSameHashInMap(underlying.v.map, hashF) + @ghost + override def valid: Boolean = + val keysList = this.keys + simpleValid && + this.map.keys().forall(k => keysList.contains(k)) + @pure @ghost def map: ListMap[K, V] = { - require(valid) + require(simpleValid) extractMap(underlying.v.map.toList) }.ensuring(res => TupleListOpsGenK.invariantList(res.toList)) diff --git a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableMapsInterface.scala b/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableMapsInterface.scala index fef66172..5966936e 100644 --- a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableMapsInterface.scala +++ b/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableMapsInterface.scala @@ -91,6 +91,7 @@ object MutableMapInterface{ @pure def size: Int + @pure def isEmpty: Boolean = { require(valid) @@ -118,5 +119,10 @@ object MutableMapInterface{ require(valid) ??? : Boolean }.ensuring(res => valid && (if (res) then abstractMap.eq(old(this).abstractMap - key) else abstractMap.eq(old(this).abstractMap))) + + def getKeys(): List[K] = { + require(valid) + ??? : List[K] + }.ensuring(res => valid && ListSpecs.noDuplicate(res) && res.content == abstractMap.keys().content) } }