From e71a3ad978ca2f2433618e1f1e3eca2c157b96a6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Wed, 28 Mar 2012 22:46:28 +0000
Subject: [PATCH] Maybe need some sort of induction to prove map acc.?
---
mytest/Abs.scala | 22 +++++++++++++---------
1 file changed, 13 insertions(+), 9 deletions(-)
diff --git a/mytest/Abs.scala b/mytest/Abs.scala
index 39bd4abb8..73e5453e1 100644
--- a/mytest/Abs.scala
+++ b/mytest/Abs.scala
@@ -4,20 +4,24 @@ object Abs {
def abs(tab: Map[Int, Int], size: Int, j: Int): Map[Int, Int] = ({
- require(j >= 0 && j < size && size > 0)
+ require(j >= 0 && j < size)
var k = 0
var tabres = Map.empty[Int, Int]
(while(k < size) {
- if(tab.isDefinedAt(k)) {
- if(tab(k) < 0)
- tabres = tabres.updated(k, -tab(k))
- else
- tabres = tabres.updated(k, tab(k))
- } else
- tabres = tabres.updated(k, 0)
+ if(tab(k) < 0)
+ tabres = tabres.updated(k, -tab(k))
+ else
+ tabres = tabres.updated(k, tab(k))
k = k + 1
- }) invariant(k >= 0 && (if(j < k) tabres(j) >= 0 else true))
+ }) invariant(k >= 0 && k <= size && (if(j < k) tabres(j) >= 0 else true))
tabres
}) ensuring(res => res(j) >= 0)
+ def isArray(a: Map[Int, Int], size: Int): Boolean = {
+ def rec(i: Int): Boolean = if(i >= size) true else {
+ if(a.isDefinedAt(i)) rec(i+1) else false
+ }
+ size > 0 && rec(0)
+ }
+
}
--
GitLab