From 4d8b7cb3c56ba286e6765becb127ffca2ea2e831 Mon Sep 17 00:00:00 2001
From: Samuel Chassot <samuel.chassot@epfl.ch>
Date: Thu, 8 Aug 2024 09:42:43 +0200
Subject: [PATCH] mini trait with postcondition

---
 modularity/MiniMutSet.scala  | 11 ++++++-----
 modularity/iMiniMutSet.scala | 23 ++++++++++++-----------
 2 files changed, 18 insertions(+), 16 deletions(-)

diff --git a/modularity/MiniMutSet.scala b/modularity/MiniMutSet.scala
index 1ad38e6a..2fc8259d 100644
--- a/modularity/MiniMutSet.scala
+++ b/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
diff --git a/modularity/iMiniMutSet.scala b/modularity/iMiniMutSet.scala
index 98727f7e..99733c0b 100644
--- a/modularity/iMiniMutSet.scala
+++ b/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))
   }