Mini Set implementation to diagnose trait and laws or empty method

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

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