diff --git a/mytest/Abs.scala b/mytest/Abs.scala index 39bd4abb80497d70d61d38946b18f1344d12ed31..73e5453e197fa015e6ec125d2a2736fa343bda32 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) + } + }