From ce5afc1279ae502cb0ddcf16ec0041a1fe7fe4dc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Sun, 6 May 2012 20:37:56 +0000
Subject: [PATCH] convert Abs testcase to using Array
---
testcases/Abs.scala | 38 +++++++++++++-------------------------
1 file changed, 13 insertions(+), 25 deletions(-)
diff --git a/testcases/Abs.scala b/testcases/Abs.scala
index 5efb41797..1a071ee10 100644
--- a/testcases/Abs.scala
+++ b/testcases/Abs.scala
@@ -3,22 +3,25 @@ import leon.Utils._
object Abs {
- def abs(tab: Map[Int, Int], size: Int): Map[Int, Int] = ({
- require(size <= 5 && isArray(tab, size))
+ def abs(tab: Array[Int]): Array[Int] = ({
+ require(tab.length >= 0)
var k = 0
- var tabres = Map.empty[Int, Int]
- (while(k < size) {
+ val tabres = Array.fill(tab.length)(0)
+ (while(k < tab.length) {
if(tab(k) < 0)
- tabres = tabres.updated(k, -tab(k))
+ tabres(k) = -tab(k)
else
- tabres = tabres.updated(k, tab(k))
+ tabres(k) = tab(k)
k = k + 1
- }) invariant(isArray(tabres, k) && k >= 0 && k <= size && isPositive(tabres, k))
+ }) invariant(
+ tabres.length == tab.length &&
+ k >= 0 && k <= tab.length &&
+ isPositive(tabres, k))
tabres
- }) ensuring(res => isArray(res, size) && isPositive(res, size))
+ }) ensuring(res => isPositive(res, res.length))
- def isPositive(a: Map[Int, Int], size: Int): Boolean = {
- require(size <= 10 && isArray(a, size))
+ def isPositive(a: Array[Int], size: Int): Boolean = {
+ require(a.length >= 0 && size <= a.length)
def rec(i: Int): Boolean = {
require(i >= 0)
if(i >= size)
@@ -33,19 +36,4 @@ object Abs {
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