From e96990ce165c59a46399fe689e86ec4561e0d3fd Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Tue, 6 Aug 2024 09:19:07 +0200 Subject: [PATCH 1/4] Mini Set implementation to diagnose trait and laws or empty method --- modularity/MiniMutSet.scala | 13 +++++++++++++ modularity/iMiniMutSet.scala | 26 ++++++++++++++++++++++++++ 2 files changed, 39 insertions(+) create mode 100644 modularity/MiniMutSet.scala create mode 100644 modularity/iMiniMutSet.scala diff --git a/modularity/MiniMutSet.scala b/modularity/MiniMutSet.scala new file mode 100644 index 00000000..1ad38e6a --- /dev/null +++ b/modularity/MiniMutSet.scala @@ -0,0 +1,13 @@ +package modularity + +import stainless.collection._ +import stainless.lang._ +import stainless.annotation._ + +object MiniMutableSet: + + @mutable + final case class MiniMutSet[V](private var content: List[V]) extends MiniMutableSetInterface.MiniMutableSet[V]: + override def contains(v: V): Boolean = content.contains(v) + override def add(v: V): Unit = content = v :: content +end MiniMutableSet diff --git a/modularity/iMiniMutSet.scala b/modularity/iMiniMutSet.scala new file mode 100644 index 00000000..0e76bd4c --- /dev/null +++ b/modularity/iMiniMutSet.scala @@ -0,0 +1,26 @@ +package modularity + + +import stainless.collection._ +import stainless.lang._ +import stainless.annotation._ + + +object MiniMutableSetInterface: + @mutable + trait MiniMutableSet[V]: + @pure def contains(v: V): Boolean + def add(v: V): Unit = { + ??? : Unit + }.ensuring(_ => contains(v)) + end MiniMutableSet +end MiniMutableSetInterface + + +object MiniSetUsage: + import MiniMutableSetInterface._ + def testMiniMutableSet(s: MiniMutableSet[BigInt]): Unit = { + s.add(1) + assert(s.contains(1)) + } +end MiniSetUsage From 28bd7f71be1996e2e986d0939a1350c20d94e8e9 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Tue, 6 Aug 2024 09:21:43 +0200 Subject: [PATCH 2/4] add a law --- modularity/iMiniMutSet.scala | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/modularity/iMiniMutSet.scala b/modularity/iMiniMutSet.scala index 0e76bd4c..98727f7e 100644 --- a/modularity/iMiniMutSet.scala +++ b/modularity/iMiniMutSet.scala @@ -13,6 +13,12 @@ object MiniMutableSetInterface: def add(v: V): Unit = { ??? : Unit }.ensuring(_ => contains(v)) + + @law @pure @ghost def addContains(v: V): Boolean = { + val snap = snapshot(this) + snap.add(v) + snap.contains(v) + } end MiniMutableSet end MiniMutableSetInterface From 4d8b7cb3c56ba286e6765becb127ffca2ea2e831 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Thu, 8 Aug 2024 09:42:43 +0200 Subject: [PATCH 3/4] mini trait with postcondition --- modularity/MiniMutSet.scala | 11 ++++++----- modularity/iMiniMutSet.scala | 23 ++++++++++++----------- 2 files changed, 18 insertions(+), 16 deletions(-) diff --git a/modularity/MiniMutSet.scala b/modularity/MiniMutSet.scala index 1ad38e6a..2fc8259d 100644 --- a/modularity/MiniMutSet.scala +++ b/modularity/MiniMutSet.scala @@ -1,13 +1,14 @@ package modularity -import stainless.collection._ -import stainless.lang._ -import stainless.annotation._ +import stainless.collection.List +import stainless.annotation.mutable object MiniMutableSet: @mutable - final case class MiniMutSet[V](private var content: List[V]) extends MiniMutableSetInterface.MiniMutableSet[V]: + final case class MiniMutSet[V](private var content: List[V]) extends MiniMutableSetInterface.iMiniMutableSet[V]: override def contains(v: V): Boolean = content.contains(v) - override def add(v: V): Unit = content = v :: content + override def add(v: V): Unit = { + content = v :: content + }.ensuring(_ => true) end MiniMutableSet diff --git a/modularity/iMiniMutSet.scala b/modularity/iMiniMutSet.scala index 98727f7e..99733c0b 100644 --- a/modularity/iMiniMutSet.scala +++ b/modularity/iMiniMutSet.scala @@ -1,31 +1,32 @@ package modularity -import stainless.collection._ -import stainless.lang._ -import stainless.annotation._ +import stainless.annotation.mutable +import stainless.annotation.pure +import stainless.annotation.law + object MiniMutableSetInterface: @mutable - trait MiniMutableSet[V]: + trait iMiniMutableSet[V]: @pure def contains(v: V): Boolean def add(v: V): Unit = { ??? : Unit }.ensuring(_ => contains(v)) - @law @pure @ghost def addContains(v: V): Boolean = { - val snap = snapshot(this) - snap.add(v) - snap.contains(v) - } - end MiniMutableSet + // @law @pure @ghost def addContains(v: V): Boolean = { + // val snap = snapshot(this) + // snap.add(v) + // snap.contains(v) + // } + end iMiniMutableSet end MiniMutableSetInterface object MiniSetUsage: import MiniMutableSetInterface._ - def testMiniMutableSet(s: MiniMutableSet[BigInt]): Unit = { + def testMiniMutableSet(s: iMiniMutableSet[BigInt]): Unit = { s.add(1) assert(s.contains(1)) } From 48b2f7fa5740b0056039d1d5f5bdf99d51a3a58b Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Thu, 12 Dec 2024 11:33:33 +0100 Subject: [PATCH 4/4] renaming files --- modularity/{MiniMutSet.scala => MiniMutableSet.scala} | 0 modularity/{iMiniMutSet.scala => MiniMutableSetInterface.scala} | 0 modularity/{iMutableSet.scala => MutableSetInterface.scala} | 0 3 files changed, 0 insertions(+), 0 deletions(-) rename modularity/{MiniMutSet.scala => MiniMutableSet.scala} (100%) rename modularity/{iMiniMutSet.scala => MiniMutableSetInterface.scala} (100%) rename modularity/{iMutableSet.scala => MutableSetInterface.scala} (100%) diff --git a/modularity/MiniMutSet.scala b/modularity/MiniMutableSet.scala similarity index 100% rename from modularity/MiniMutSet.scala rename to modularity/MiniMutableSet.scala diff --git a/modularity/iMiniMutSet.scala b/modularity/MiniMutableSetInterface.scala similarity index 100% rename from modularity/iMiniMutSet.scala rename to modularity/MiniMutableSetInterface.scala diff --git a/modularity/iMutableSet.scala b/modularity/MutableSetInterface.scala similarity index 100% rename from modularity/iMutableSet.scala rename to modularity/MutableSetInterface.scala