From d2a5eb79a6f580f09a7f4707647855ba111ae360 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Fri, 4 May 2012 13:53:54 +0200
Subject: [PATCH] convert testcases from Map to Array
---
testcases/LinearSearch.scala | 40 ++++++++++--------------------
testcases/MaxSum.scala | 48 ++++++------------------------------
2 files changed, 21 insertions(+), 67 deletions(-)
diff --git a/testcases/LinearSearch.scala b/testcases/LinearSearch.scala
index e91a3f267..e18c4039c 100644
--- a/testcases/LinearSearch.scala
+++ b/testcases/LinearSearch.scala
@@ -4,29 +4,29 @@ import leon.Utils._
object LinearSearch {
- def linearSearch(a: Map[Int, Int], size: Int, c: Int): Boolean = ({
- require(size <= 5 && isArray(a, size))
+ def linearSearch(a: Array[Int], c: Int): Boolean = ({
+ require(a.length >= 0)
var i = 0
var found = false
- (while(i < size) {
+ (while(i < a.length) {
if(a(i) == c)
found = true
i = i + 1
- }) invariant(i <= size &&
- i >= 0 &&
- (if(found) contains(a, i, c) else !contains(a, i, c))
- )
+ }) invariant(
+ i <= a.length &&
+ i >= 0 &&
+ (if(found) contains(a, i, c) else !contains(a, i, c))
+ )
found
- }) ensuring(res => if(res) contains(a, size, c) else !contains(a, size, c))
+ }) ensuring(res => if(res) contains(a, a.length, c) else !contains(a, a.length, c))
- def contains(a: Map[Int, Int], size: Int, c: Int): Boolean = {
- require(isArray(a, size) && size <= 5)
+ def contains(a: Array[Int], size: Int, c: Int): Boolean = {
+ require(a.length >= 0 && size >= 0 && size <= a.length)
content(a, size).contains(c)
}
-
- def content(a: Map[Int, Int], size: Int): Set[Int] = {
- require(isArray(a, size) && size <= 5)
+ def content(a: Array[Int], size: Int): Set[Int] = {
+ require(a.length >= 0 && size >= 0 && size <= a.length)
var set = Set.empty[Int]
var i = 0
(while(i < size) {
@@ -36,18 +36,4 @@ object LinearSearch {
set
}
- def isArray(a: Map[Int, Int], size: Int): Boolean = {
-
- def rec(i: Int): Boolean = {
- require(i >= 0)
- if(i >= size) true else {
- if(a.isDefinedAt(i)) rec(i+1) else false
- }
- }
-
- if(size < 0)
- false
- else
- rec(0)
- }
}
diff --git a/testcases/MaxSum.scala b/testcases/MaxSum.scala
index 07c5d12ab..ba724d255 100644
--- a/testcases/MaxSum.scala
+++ b/testcases/MaxSum.scala
@@ -4,44 +4,26 @@ import leon.Utils._
object MaxSum {
-
- def maxSum(a: Map[Int, Int], size: Int): (Int, Int) = ({
- require(isArray(a, size) && size < 5 && isPositive(a, size))
+ def maxSum(a: Array[Int]): (Int, Int) = ({
+ require(a.length >= 0 && isPositive(a))
var sum = 0
var max = 0
var i = 0
- (while(i < size) {
+ (while(i < a.length) {
if(max < a(i))
max = a(i)
sum = sum + a(i)
i = i + 1
- }) invariant (sum <= i * max && /*isGreaterEq(a, i, max) &&*/ /*(if(i == 0) max == 0 else true) &&*/ i >= 0 && i <= size)
+ }) invariant (sum <= i * max && i >= 0 && i <= a.length)
(sum, max)
- }) ensuring(res => res._1 <= size * res._2)
+ }) ensuring(res => res._1 <= a.length * res._2)
-/*
- def isGreaterEq(a: Map[Int, Int], size: Int, n: Int): Boolean = {
- require(size <= 5 && isArray(a, size))
- def rec(i: Int): Boolean = {
- require(i >= 0)
- if(i >= size)
- true
- else {
- if(a(i) > n)
- false
- else
- rec(i+1)
- }
- }
- rec(0)
- }
- */
- def isPositive(a: Map[Int, Int], size: Int): Boolean = {
- require(size <= 5 && isArray(a, size))
+ def isPositive(a: Array[Int]): Boolean = {
+ require(a.length >= 0)
def rec(i: Int): Boolean = {
require(i >= 0)
- if(i >= size)
+ if(i >= a.length)
true
else {
if(a(i) < 0)
@@ -53,18 +35,4 @@ object MaxSum {
rec(0)
}
- def isArray(a: Map[Int, Int], size: Int): Boolean = {
-
- def rec(i: Int): Boolean = {
- require(i >= 0)
- if(i >= size) true else {
- if(a.isDefinedAt(i)) rec(i+1) else false
- }
- }
-
- if(size < 0)
- false
- else
- rec(0)
- }
}
--
GitLab