From 8d770dc9aef7dd9105c60fbcf1db6fb25fcabbc5 Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <viktor.kuncak@epfl.ch>
Date: Mon, 5 Aug 2024 22:24:50 +0200
Subject: [PATCH 1/2] Example of using abstract classes. Requires stainless to
 detect when methods are abstract by way of containing ??? symbol

---
 .../MutableSet.scala                          | 42 ++++++++++++++++++
 .../iMutableSet.scala                         | 44 +++++++++++++++++++
 .../list-nodup-abstract-class/stainless.conf  | 15 +++++++
 3 files changed, 101 insertions(+)
 create mode 100644 data-structures/mutable-set/list-nodup-abstract-class/MutableSet.scala
 create mode 100644 data-structures/mutable-set/list-nodup-abstract-class/iMutableSet.scala
 create mode 100644 data-structures/mutable-set/list-nodup-abstract-class/stainless.conf

diff --git a/data-structures/mutable-set/list-nodup-abstract-class/MutableSet.scala b/data-structures/mutable-set/list-nodup-abstract-class/MutableSet.scala
new file mode 100644
index 00000000..31c3e951
--- /dev/null
+++ b/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
diff --git a/data-structures/mutable-set/list-nodup-abstract-class/iMutableSet.scala b/data-structures/mutable-set/list-nodup-abstract-class/iMutableSet.scala
new file mode 100644
index 00000000..06bbaf7b
--- /dev/null
+++ b/data-structures/mutable-set/list-nodup-abstract-class/iMutableSet.scala
@@ -0,0 +1,44 @@
+package modularity
+
+
+import stainless.collection._
+import stainless.lang._
+import stainless.annotation._
+
+
+object MutableSetObj:
+  @mutable
+  trait MutableSet[V]:
+    @pure
+    def toSet: 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
+end MutableSetObj
diff --git a/data-structures/mutable-set/list-nodup-abstract-class/stainless.conf b/data-structures/mutable-set/list-nodup-abstract-class/stainless.conf
new file mode 100644
index 00000000..1398cc41
--- /dev/null
+++ b/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"

From f10df7d68a55aa3097f22ec97a21366b10a8f7ac Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <viktor.kuncak@epfl.ch>
Date: Mon, 5 Aug 2024 22:32:45 +0200
Subject: [PATCH 2/2] Also made toSet non-abstract from the point of dotty

---
 .../list-nodup-abstract-class/iMutableSet.scala          | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/data-structures/mutable-set/list-nodup-abstract-class/iMutableSet.scala b/data-structures/mutable-set/list-nodup-abstract-class/iMutableSet.scala
index 06bbaf7b..a0dbe629 100644
--- a/data-structures/mutable-set/list-nodup-abstract-class/iMutableSet.scala
+++ b/data-structures/mutable-set/list-nodup-abstract-class/iMutableSet.scala
@@ -10,7 +10,9 @@ object MutableSetObj:
   @mutable
   trait MutableSet[V]:
     @pure
-    def toSet: Set[V]
+    def toSet: Set[V] = {
+      ??? : Set[V]
+    }
 
     @pure
     def contains(v: V): Boolean = {
@@ -41,4 +43,9 @@ object MutableSetObj:
     } ensuring(_ >= 0)
 
   end MutableSet
+
+  def test =
+    val ms = new MutableSet[Int] {}
+    true
+
 end MutableSetObj