Example of abstraction using methods with ???. Needs some systematic checks for missing implementations

data-structures/mutable-set/list-nodup-abstract-class/MutableSet.scala

@@ -0,0 +1,42 @@
+package modularity
+
+import stainless.collection._
+import stainless.lang._
+import stainless.annotation._
+
+object MutableSetImplObj:
+
+  @mutable
+  final case class MutableSetImpl[V](private var list: List[V]) extends MutableSetObj.MutableSet[V]:
+    require(ListSpecs.noDuplicate(list))
+
+    override def toSet = list.content
+
+    override def contains(v: V): Boolean = list.contains(v)
+
+    override def add(v: V): Unit =
+      if !list.contains(v) then
+        list = v :: list
+      else 
+        ()
+
+    override def remove(v: V): Unit = 
+      list = removeElement(list, v)
+
+    private def removeElement(l: List[V], v: V): List[V] = {
+      require(ListSpecs.noDuplicate(l))
+      l match
+        case Nil() => Nil[V]()
+        case Cons(h, t) if h == v => t
+        case Cons(h, t) => Cons(h, removeElement(t, v))
+      }.ensuring(res =>
+        !res.contains(v)
+        && ListSpecs.noDuplicate(res)
+        && res.content == l.content -- Set(v)
+        && (if l.contains(v) then res.size == l.size - 1 else res.size == l.size)
+    )
+
+    override def size: BigInt = 
+      list.size
+
+end MutableSetImplObj

data-structures/mutable-set/list-nodup-abstract-class/iMutableSet.scala

@@ -0,0 +1,51 @@
+package modularity
+
+
+import stainless.collection._
+import stainless.lang._
+import stainless.annotation._
+
+
+object MutableSetObj:
+  @mutable
+  trait MutableSet[V]:
+    @pure
+    def toSet: Set[V] = {
+      ??? : Set[V]
+    }
+
+    @pure
+    def contains(v: V): Boolean = {
+      ??? : Boolean
+    } ensuring(_ == toSet.contains(v))
+
+    def add(v: V): Unit = {
+      ??? : Unit
+    } ensuring(() => 
+        toSet == old(this).toSet + v &&
+        (if old(this).contains(v) then 
+          size == old(this).size
+        else
+          size == old(this).size + 1))
+
+    def remove(v: V): Unit = {
+      ??? : Unit
+    } ensuring(() => 
+        toSet == old(this).toSet - v &&
+        (if old(this).contains(v) then 
+          size == old(this).size - 1
+        else
+          size == old(this).size))
+
+    @pure
+    def size: BigInt = {
+      ??? : BigInt
+    } ensuring(_ >= 0)
+
+  end MutableSet
+
+  def test =
+    val ms = new MutableSet[Int] {}
+    true
+
+end MutableSetObj

data-structures/mutable-set/list-nodup-abstract-class/stainless.conf

@@ -0,0 +1,15 @@
+# The settings below correspond to the various
+# options listed by `stainless --help`
+
+vc-cache            = true
+# debug               = ["verification", "smt"]
+timeout             = 15
+check-models        = false
+print-ids           = false
+print-types         = false
+batched             = true
+strict-arithmetic   = false
+solvers             = "smt-cvc5,smt-z3,smt-cvc4"
+check-measures      = yes
+infer-measures      = true
+simplifier           = "ol"