From e0008d58f89d459db899252fde8ba37587b670c7 Mon Sep 17 00:00:00 2001 From: Mario Bucev Date: Mon, 21 Mar 2022 10:35:35 +0100 Subject: [PATCH] Update SortedArray benchmark --- .../sorted-array/SortedArray.scala | 30 +++++++++---------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/data-structures/sorted-array/SortedArray.scala b/data-structures/sorted-array/SortedArray.scala index 2f3b32f1..25e72335 100644 --- 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,7 +93,7 @@ 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)) @@ -101,7 +101,7 @@ object SortedArray { }.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)) }