mini trait with postcondition

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

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))
   }