From 62ede09ee7c648b89520f6a24a9cf3c64d2ed230 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Wed, 28 Mar 2012 16:47:15 +0200
Subject: [PATCH] Ok now it's working on the Abs example !
---
mytest/Abs.scala | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/mytest/Abs.scala b/mytest/Abs.scala
index d18929903..39bd4abb8 100644
--- a/mytest/Abs.scala
+++ b/mytest/Abs.scala
@@ -13,9 +13,8 @@ object Abs {
tabres = tabres.updated(k, -tab(k))
else
tabres = tabres.updated(k, tab(k))
- } else {
+ } else
tabres = tabres.updated(k, 0)
- }
k = k + 1
}) invariant(k >= 0 && (if(j < k) tabres(j) >= 0 else true))
tabres
--
GitLab