migration to 3.5

tutorials/dispenser/Dispenser.scala

@@ -75,8 +75,8 @@ object Dispenser {
         List(b10,b10,b10,b10)),
       coins = BigInt(0),
       oneInserted=false)
-    val Some(s1) = r(s0, FirstCoin())
-    val Some(s2) = r(s1, SecondCoin(0,0))
+    val Some(s1) = r(s0, FirstCoin()): @unchecked
+    val Some(s2) = r(s1, SecondCoin(0,0)): @unchecked
     List[(State,Action)]((s0, FirstCoin()), (s1, SecondCoin(0,0)), (s2, FirstCoin()))
   }.ensuring(res => isTrace(res))
 

tutorials/krakow2020/IntSet.scala

@@ -9,21 +9,21 @@ sealed abstract class IntSet {
     def incl(x: Int): IntSet = this match {
         case Empty() => Node(Empty(),x,Empty())
         case Node(left, elem, right) =>
-          if (x < elem) Node(left incl x, elem, right)
-          else if (x > elem) Node(left, elem, right incl x)
+          if (x < elem) Node(left.incl(x), elem, right)
+          else if (x > elem) Node(left, elem, right.incl(x))
           else this
     }
     def contains(x: Int): Boolean = this match {
         case Empty() => false
         case Node(left, elem, right) =>
-          if (x < elem) left contains x
-          else if (x > elem) right contains x
+          if (x < elem) left.contains(x)
+          else if (x > elem) right.contains(x)
           else true
     }
 
     def P1(x: Int): Boolean = {
         true
-    }.ensuring(_ => !(Empty() contains x))
+    }.ensuring(_ => !(Empty().contains(x)))
 
     def P2(s: IntSet, x: Int): Boolean = {
         s match {
@@ -33,7 +33,7 @@ sealed abstract class IntSet {
                 else if (x > elem) P2(right, x)
                 else true
         }
-    }.ensuring(_ => (s incl x) contains x)
+    }.ensuring(_ => (s.incl(x)).contains(x))
 
     def P3(s: IntSet, x: Int,  y: Int): Boolean = {
         require(x != y)
@@ -44,11 +44,11 @@ sealed abstract class IntSet {
                 else if (x > elem) P3(right, x, y)
                 else true
         }
-    }.ensuring(_ =>  ((s incl x) contains y)==(s contains y))
+    }.ensuring(_ =>  ((s.incl(x)).contains(y))==(s.contains(y)))
 
     def union(other: IntSet): IntSet = this match {
         case Empty() => other
         case Node(left, x, right) => 
-            (left union (right union other)) incl x
+            (left.union(right.union(other))).incl(x)
     }
 }

tutorials/krakow2020/IntSetInv.scala

@@ -20,36 +20,36 @@ sealed abstract class IntSet {
     def incl(x: Int): IntSet = { this match {
         case Empty() => Node(Empty(),x,Empty())
         case Node(left, elem, right) =>
-          if (x < elem) Node(left incl x, elem, right)
-          else if (x > elem) Node(left, elem, right incl x)
+          if (x < elem) Node(left.incl(x), elem, right)
+          else if (x > elem) Node(left, elem, right.incl(x))
           else this
     }}.ensuring(res => res.content == this.content ++ Set(x))
 
     def contains(x: Int): Boolean = {this match {
         case Empty() => false
         case Node(left, elem, right) =>
-          if (x < elem) left contains x
-          else if (x > elem) right contains x
+          if (x < elem) left.contains(x)
+          else if (x > elem) right.contains(x)
           else true
     }}.ensuring(res => (res == (this.content.contains(x))))
 
     def P1(x: Int): Unit = 
     ().ensuring(_ => !(Empty().contains(x)))
 
     def P2(s: IntSet, x: Int): Unit = 
-    ().ensuring(_ => (s incl x) contains x)
+    ().ensuring(_ => (s.incl(x)).contains(x))
 
     def P3(s: IntSet, x: Int,  y: Int): Unit = {
       require(x != y)
-    }.ensuring(_ =>  ((s incl x) contains y)==(s contains y))
+    }.ensuring(_ =>  ((s.incl(x)).contains(y))==(s.contains(y)))
 
     def union(other: IntSet): IntSet = {this match {
         case Empty() => other
         case Node(left, x, right) => 
-            (left union (right union other)) incl x
+            (left.union(right.union(other))).incl(x)
     }}.ensuring(res => res.content == this.content ++ other.content)
 
     def P4(t1: IntSet, t2: IntSet, x: Int): Unit = 
-    ().ensuring(_ =>  ((t1 union t2) contains x)==
-                      (t1 contains x) || (t2 contains x))
+    ().ensuring(_ =>  ((t1.union(t2)).contains(x))==
+                      (t1.contains(x)) || (t2.contains(x)))
 }