A mutable trait example to illustrate modularising data structure pro…

…ofs; uses snapshot (#99)

* add modularity set

* working version

modularity/MutableSet.scala

@@ -0,0 +1,37 @@
+package modularity
+
+import stainless.collection._
+import stainless.lang._
+import stainless.annotation._
+
+object MutableSetImplObj:
+
+  @mutable
+  final case class MutableSetImpl[V](private var content: List[V]) extends MutableSetObj.MutableSet[V]:
+    require(ListSpecs.noDuplicate(content))
+    def contains(v: V): Boolean = content.contains(v)
+
+    def add(v: V): Unit =
+      if (!content.contains(v)) then
+        content = v :: content
+      else 
+        ()
+    def remove(v: V): Unit = content = removeElement(content, v)
+    def size: BigInt = content.size
+
+    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)
+    )
+
+
+
+end MutableSetImplObj

modularity/iMutableSet.scala

@@ -0,0 +1,51 @@
+package modularity
+
+
+import stainless.collection._
+import stainless.lang._
+import stainless.annotation._
+
+
+object MutableSetObj:
+  @mutable
+  trait MutableSet[V]:
+    def contains(v: V): Boolean
+    def add(v: V): Unit
+    def remove(v: V): Unit
+    def size: BigInt
+
+    @law @pure @ghost def addContains(v: V): Boolean =
+      val thisSnap = snapshot(this)
+      thisSnap.add(v)  
+      thisSnap.contains(v)
+
+    @law @pure @ghost def addOtherSameContains(v: V, other: V): Boolean =
+      val thisSnap = snapshot(this)
+      val thisSnapBefore = snapshot(this)
+      thisSnap.add(v)
+      if(v != other) then thisSnap.contains(other) == thisSnapBefore.contains(other) else true
+
+    @law @pure @ghost def removeNotContains(v: V): Boolean =
+      val thisSnap = snapshot(this)
+      thisSnap.remove(v)
+      !thisSnap.contains(v)
+
+    @law @pure @ghost def removeOtherSameContains(v: V, other: V): Boolean =
+      val thisSnap = snapshot(this)
+      val thisSnapBefore = snapshot(this)
+      thisSnap.remove(v)
+      if(v != other) then thisSnap.contains(other) == thisSnapBefore.contains(other) else true
+
+    @law @pure @ghost def addIncreasesSizeByOneOrWasContained(v: V): Boolean =
+      val thisSnap = snapshot(this)
+      val thisSnapBefore = snapshot(this)
+      thisSnap.add(v)
+      if(thisSnapBefore.contains(v)) then thisSnap.size == thisSnapBefore.size else thisSnap.size == thisSnapBefore.size + 1
+
+    @law @pure @ghost def removeDecreasesSizeByOneOrWasNotContained(v: V): Boolean =
+      val thisSnap = snapshot(this)
+      val thisSnapBefore = snapshot(this)
+      thisSnap.remove(v)
+      if(thisSnapBefore.contains(v)) then thisSnap.size == thisSnapBefore.size - 1 else thisSnap.size == thisSnapBefore.size
+  end MutableSet
+end MutableSetObj

modularity/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"