From fd2c6ceced56109109c1bcf4ea59e7af897c4993 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Sat, 16 Apr 2016 02:03:44 +0200
Subject: [PATCH] update some outdated xlang testcases
---
testcases/verification/xlang/MaxSum.scala | 48 +++--------------------
testcases/verification/xlang/Sums.scala | 28 +++++++++++++
2 files changed, 33 insertions(+), 43 deletions(-)
create mode 100644 testcases/verification/xlang/Sums.scala
diff --git a/testcases/verification/xlang/MaxSum.scala b/testcases/verification/xlang/MaxSum.scala
index f4d056ab9..e00ea1c12 100644
--- a/testcases/verification/xlang/MaxSum.scala
+++ b/testcases/verification/xlang/MaxSum.scala
@@ -4,8 +4,10 @@ import leon.lang._
object MaxSum {
- def maxSum(a: Array[Int]): (Int, Int) = ({
- require(a.length >= 0 && isPositive(a))
+ //not valid because of Int, unfortunately conversion between big int and
+ //int does not work and we cannot compute a.length * Max (Int * BigInt)
+ def maxSum(a: Array[Int]): (Int, Int) = {
+ require(a.length >= 0)
var sum = 0
var max = 0
var i = 0
@@ -16,46 +18,6 @@ object MaxSum {
i = i + 1
}) invariant (sum <= i * max && i >= 0 && i <= a.length)
(sum, max)
- }) ensuring(res => res._1 <= a.length * res._2)
-
-
- def isPositive(a: Array[Int]): Boolean = {
- require(a.length >= 0)
- def rec(i: Int): Boolean = {
- require(i >= 0)
- if(i >= a.length)
- true
- else {
- if(a(i) < 0)
- false
- else
- rec(i+1)
- }
- }
- rec(0)
- }
-
- def summ(to : Int): Int = ({
- require(to >= 0)
- var i = 0
- var s = 0
- (while (i < to) {
- s = s + i
- i = i + 1
- }) invariant (s >= 0 && i >= 0 && s == i*(i-1)/2 && i <= to)
- s
- }) ensuring(res => res >= 0 && res == to*(to-1)/2)
-
-
- def sumsq(to : Int): Int = ({
- require(to >= 0)
- var i = 0
- var s = 0
- (while (i < to) {
- s = s + i*i
- i = i + 1
- }) invariant (s >= 0 && i >= 0 && s == (i-1)*i*(2*i-1)/6 && i <= to)
- s
- }) ensuring(res => res >= 0 && res == (to-1)*to*(2*to-1)/6)
+ } ensuring(res => res._1 <= a.length * res._2)
}
diff --git a/testcases/verification/xlang/Sums.scala b/testcases/verification/xlang/Sums.scala
new file mode 100644
index 000000000..1d6ad2e94
--- /dev/null
+++ b/testcases/verification/xlang/Sums.scala
@@ -0,0 +1,28 @@
+import leon.lang._
+
+object Sums {
+
+ def summ(to : BigInt): BigInt = ({
+ require(to >= 0)
+ var i: BigInt = 0
+ var s: BigInt = 0
+ (while (i < to) {
+ s = s + i
+ i = i + 1
+ }) invariant (s >= 0 && i >= 0 && s == i*(i-1)/2 && i <= to)
+ s
+ }) ensuring(res => res >= 0 && res == to*(to-1)/2)
+
+
+ def sumsq(to : BigInt): BigInt = ({
+ require(to >= 0)
+ var i: BigInt = 0
+ var s: BigInt = 0
+ (while (i < to) {
+ s = s + i*i
+ i = i + 1
+ }) invariant (s >= 0 && i >= 0 && s == (i-1)*i*(2*i-1)/6 && i <= to)
+ s
+ }) ensuring(res => res >= 0 && res == (to-1)*to*(2*to-1)/6)
+
+}
--
GitLab