From a61a9ffe87fd30b0c485b884a558454b1853a9a3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Wed, 28 Mar 2012 15:22:24 +0200
Subject: [PATCH] Simple program involving arrays
---
mytest/Abs.scala | 21 +++++++++++++++++++++
1 file changed, 21 insertions(+)
create mode 100644 mytest/Abs.scala
diff --git a/mytest/Abs.scala b/mytest/Abs.scala
new file mode 100644
index 000000000..3774d5daa
--- /dev/null
+++ b/mytest/Abs.scala
@@ -0,0 +1,21 @@
+import leon.Utils._
+
+object Abs {
+
+
+ def abs(tab: Map[Int, Int], size: Int, j: Int): Map[Int, Int] = {
+ require(j >= 0 && j < size && tab.isDefinedAt(j) && size > 0)
+ var k = 0
+ var tabres = Map.empty[Int, Int]
+ (while(k < size) {
+ if(tab(k) < 0)
+ tabres = tabres.updated(k, -tab(k))
+ else
+ tabres = tabres.updated(k, tab(k))
+ k = k + 1
+ }) invariant(k >= 0)
+ tabres
+
+ }
+
+}
--
GitLab