From d70f5b6be27eff5965576b62edc96d8a3e1b0328 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Mon, 14 Oct 2024 16:28:35 +0200 Subject: [PATCH 1/4] work on the keys operation on map --- .../scala/ch/epfl/map/MutableHashMap.scala | 22 ++++++++++++++----- .../ch/epfl/map/MutableMapsInterface.scala | 10 ++++++++- 2 files changed, 26 insertions(+), 6 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 index 4ec56b9c..be58fc59 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 @@ -48,7 +49,7 @@ object MutableHashMap { @ghost override def abstractMap: ListMap[K, V] = { - require(valid) + require(simpleValid) this.map } @@ -146,7 +147,9 @@ object MutableHashMap { check(underlying.v.map.toList.forall((k, v) => noDuplicateKeys(v))) check(allKeysSameHashInMap(underlying.v.map, hashF)) check(map.eq(oldMap + (key, v))) + check(keys.contains(key)) } else { + check(keys.contains(key)) check(valid) check(map == oldMap) } @@ -176,6 +179,7 @@ object MutableHashMap { ListMapLemmas.lemmaEquivalentThenSameContains(map, oldMap + (key, v), key) check((oldMap + (key, v)).contains(key)) check(map.contains(key)) + check(keys.contains(key)) } else { check(valid) check(map == oldMap) @@ -232,15 +236,23 @@ object MutableHashMap { }.ensuring (res => valid && (if (res) map.eq(old(this).map - key) else map.eq(old(this).map))) - @ghost - override def valid: Boolean = underlying.v.valid && + @ghost + 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.abstractMap.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..fe984eb4 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 @@ -69,6 +69,14 @@ object MutableMapInterface{ @mutable trait MutableMap[K, V] { import ch.epfl.map.ListMap + + /** + * Invariant for the datastructure needed to construct the abstractMap + */ + @pure + @ghost + def simpleValid: Boolean + /** * Invariant for the datastructure */ @@ -85,7 +93,7 @@ object MutableMapInterface{ @ghost @pure def abstractMap: ListMap[K, V] = { - require(valid) + require(simpleValid) ??? : ListMap[K, V] } From c8f717350745e60dcaf6c03a81693db17dc35ffc Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Tue, 15 Oct 2024 17:20:45 +0200 Subject: [PATCH 2/4] add getKeys (proved until filtering) --- .../src/main/scala/ch/epfl/map/ListMap.scala | 57 +++++++++---- .../scala/ch/epfl/map/MutableHashMap.scala | 79 +++++++++++++++++-- .../ch/epfl/map/MutableMapsInterface.scala | 16 ++-- 3 files changed, 120 insertions(+), 32 deletions(-) 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 be58fc59..32ad8a26 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 @@ -49,7 +49,7 @@ object MutableHashMap { @ghost override def abstractMap: ListMap[K, V] = { - require(simpleValid) + require(valid) this.map } @@ -124,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) { @@ -147,11 +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 @@ -164,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) { @@ -180,13 +202,27 @@ object MutableHashMap { 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 @@ -222,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) @@ -236,18 +279,40 @@ object MutableHashMap { }.ensuring (res => valid && (if (res) map.eq(old(this).map - key) else map.eq(old(this).map))) - @ghost + override def getKeys(): List[K] = { + require(valid) + filterKeys(keys) + }.ensuring(res => valid && ListSpecs.noDuplicate(res) && res.content == map.keys().content) + + // TODO tailrec version + @pure + def filterKeys(l: List[K]): List[K] = { + require(ListSpecs.noDuplicate(l)) + decreases(l) + l match { + case Cons(hd, tl) if contains(hd) => Cons(hd, filterKeys(tl)) + case Cons(_, tl) => filterKeys(tl) + case Nil() => Nil() + } + + }.ensuring(res => + val aMap = map + ListSpecs.noDuplicate(res) + && res.content.subsetOf(l.content) + && res.forall(k => aMap.contains(k))) + + @ghost + @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 = + override def valid: Boolean = val keysList = this.keys simpleValid && - this.abstractMap.keys().forall(k => keysList.contains(k)) - + this.map.keys().forall(k => keysList.contains(k)) @pure @ghost 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 fe984eb4..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 @@ -69,14 +69,6 @@ object MutableMapInterface{ @mutable trait MutableMap[K, V] { import ch.epfl.map.ListMap - - /** - * Invariant for the datastructure needed to construct the abstractMap - */ - @pure - @ghost - def simpleValid: Boolean - /** * Invariant for the datastructure */ @@ -93,12 +85,13 @@ object MutableMapInterface{ @ghost @pure def abstractMap: ListMap[K, V] = { - require(simpleValid) + require(valid) ??? : ListMap[K, V] } @pure def size: Int + @pure def isEmpty: Boolean = { require(valid) @@ -126,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) } } From 87c094e4306fbdac9ef4baa1d00011048df514b7 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Wed, 16 Oct 2024 08:41:52 +0200 Subject: [PATCH 3/4] tail rec filter --- .../main/scala/ch/epfl/map/MutableHashMap.scala | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 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 index 32ad8a26..05495fb4 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 @@ -286,13 +286,18 @@ object MutableHashMap { // TODO tailrec version @pure - def filterKeys(l: List[K]): List[K] = { - require(ListSpecs.noDuplicate(l)) + def filterKeys(l: List[K], acc: List[K] = Nil()): List[K] = { + require(valid) + require({ + val aMap = map + acc.forall(k => aMap.contains(k)) + }) + require(ListSpecs.subseq(acc, l)) decreases(l) l match { - case Cons(hd, tl) if contains(hd) => Cons(hd, filterKeys(tl)) - case Cons(_, tl) => filterKeys(tl) - case Nil() => Nil() + case Cons(hd, tl) if this.contains(hd) && !acc.contains(hd) => filterKeys(tl, Cons(hd, acc)) + case Cons(_, tl) => filterKeys(tl, acc) + case Nil() => acc } }.ensuring(res => From b736921c653c8cf0fe0c787dbe9bdea3a7c59613 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Wed, 16 Oct 2024 17:09:28 +0200 Subject: [PATCH 4/4] working on getkeys --- .../scala/ch/epfl/map/MutableHashMap.scala | 21 +++++++++++++++---- 1 file changed, 17 insertions(+), 4 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 index 05495fb4..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 @@ -284,7 +284,6 @@ object MutableHashMap { filterKeys(keys) }.ensuring(res => valid && ListSpecs.noDuplicate(res) && res.content == map.keys().content) - // TODO tailrec version @pure def filterKeys(l: List[K], acc: List[K] = Nil()): List[K] = { require(valid) @@ -292,11 +291,25 @@ object MutableHashMap { val aMap = map acc.forall(k => aMap.contains(k)) }) - require(ListSpecs.subseq(acc, l)) + 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) => filterKeys(tl, Cons(hd, acc)) - case Cons(_, tl) => filterKeys(tl, acc) + 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 }