diff --git a/testcases/BubbleSort.scala b/testcases/BubbleSort.scala index f807c1b8589b62b1a3eaf669509a20af4982e531..5249f4fbe33f31ef8b963d3652b7e26747347629 100644 --- a/testcases/BubbleSort.scala +++ b/testcases/BubbleSort.scala @@ -22,6 +22,7 @@ object BubbleSort { j >= 0 && j <= i && i < sa.length && + sa.length >= 0 && partitioned(sa, 0, i, i+1, sa.length-1) && sorted(sa, i, sa.length-1) && partitioned(sa, 0, j-1, j, j) @@ -30,6 +31,7 @@ object BubbleSort { }) invariant( i >= 0 && i < sa.length && + sa.length >= 0 && partitioned(sa, 0, i, i+1, sa.length-1) && sorted(sa, i, sa.length-1) )