Update SortedArray benchmark

epfl-lara · Mar 21, 2022 · e0008d5 · e0008d5
1 parent 155ccc3
commit e0008d5
Showing 1 changed file with 15 additions and 15 deletions.
diff --git a/data-structures/sorted-array/SortedArray.scala b/data-structures/sorted-array/SortedArray.scala
@@ -76,7 +76,7 @@ object SortedArray {
     }
 
   }.ensuring(_ =>
-    isSortedRange(array.updated(j, array(j-1)).updated(j-1, array(j)), order, i, j-1)
+    isSortedRange(array.updated(j, snapshot(array(j-1))).updated(j-1, snapshot(array(j))), order, i, j-1)
   )
 
   @pure @opaque @ghostAnnot @inlineOnce
@@ -93,15 +93,15 @@ object SortedArray {
 
     if (0 <= i && i < array.length - 1 && i < j) {
       isSortedRangeSwap2(array, order, i+1, j, k, l)
-      val ar: Array[(K, T)] = array.updated(k, array(l)).updated(l, array(k))
+      val ar: Array[(K, T)] = array.updated(k, snapshot(array(l))).updated(l, snapshot(array(k)))
       assert(isSortedRange(ar, order, i+1, j))
       assert(order.leq(ar(i)._1, ar(i+1)._1))
       check(isSortedRange(ar, order, i, j))
     }
 
 
   }.ensuring(_ =>
-    isSortedRange(array.updated(k, array(l)).updated(l, array(k)), order, i, j)
+    isSortedRange(array.updated(k, snapshot(array(l))).updated(l, snapshot(array(k))), order, i, j)
   )
 
   @pure @opaque @ghostAnnot @inlineOnce
@@ -218,25 +218,25 @@ object SortedArray {
       if (i < h) {
         sortedRangePair(array, order, i, 0, h)
         assert(order.leq(array(i)._1, array(i + 1)._1))
-        assert(order.leq(array.updated(h, elem).apply(i)._1, array.updated(h, elem).apply(i + 1)._1))
-        assert(isSortedRange(array.updated(h, elem), order, i+1, array.length - 1))
-        check(isSortedRange(array.updated(h, elem), order, i, array.length - 1))
+        assert(order.leq(array.updated(h, snapshot(elem)).apply(i)._1, array.updated(h, snapshot(elem)).apply(i + 1)._1))
+        assert(isSortedRange(array.updated(h, snapshot(elem)), order, i+1, array.length - 1))
+        check(isSortedRange(array.updated(h, snapshot(elem)), order, i, array.length - 1))
       }
       else if (i >= h+1) {
         sortedRangePair(array, order, i, h+1, array.length-1)
-        assert(isSortedRange(array.updated(h, elem), order, i + 1, array.length - 1))
+        assert(isSortedRange(array.updated(h, snapshot(elem)), order, i + 1, array.length - 1))
         assert(order.leq(
-          (array.updated(h, elem): Array[(K, T)])(i)._1,
-          (array.updated(h, elem): Array[(K, T)])(i+1)._1
+          (array.updated(h, snapshot(elem)): Array[(K, T)])(i)._1,
+          (array.updated(h, snapshot(elem)): Array[(K, T)])(i+1)._1
         ))
-        check(isSortedRange(array.updated(h, elem), order, i, array.length - 1))
+        check(isSortedRange(array.updated(h, snapshot(elem)), order, i, array.length - 1))
       } else {
-        check(isSortedRange(array.updated(h, elem), order, i, array.length - 1))
+        check(isSortedRange(array.updated(h, snapshot(elem)), order, i, array.length - 1))
       }
     }
 
   }.ensuring { _ =>
-    isSortedRange(array.updated(h, elem), order, i, array.length - 1)
+    isSortedRange(array.updated(h, snapshot(elem)), order, i, array.length - 1)
   }
 
   @opaque @ghostAnnot @pure @inlineOnce
@@ -250,7 +250,7 @@ object SortedArray {
     insertSortedRange(array, order, h, elem, 0)
 
   }.ensuring { _ =>
-    isSorted(array.updated(h, elem), order)
+    isSorted(array.updated(h, snapshot(elem)), order)
   }
 
   @opaque @pure
@@ -391,8 +391,8 @@ case class SortedArray[K, @mutable T](array: Array[(K, T)], order: TotalOrder[K]
           assert(order.leq(array(i-2)._1, array(i-1)._1))
         }
         isSortedRangeSwap2(array, order, i+1, array.length-1, i, i-1)
-        assert(isSortedRange(array.updated(i, array(i-1)).updated(i-1, array(i)), order, i+1, array.length-1))
-        check(isSortedRange(array.updated(i, array(i-1)).updated(i-1, array(i)), order, i+2, array.length-1))
+        assert(isSortedRange(array.updated(i, snapshot(array(i-1))).updated(i-1, snapshot(array(i))), order, i+1, array.length-1))
+        check(isSortedRange(array.updated(i, snapshot(array(i-1))).updated(i-1, snapshot(array(i))), order, i+2, array.length-1))
         assert((i > h && h < n) ==> order.leq(elem._1, array(h)._1))
       }