From 1698c252275ffa00c2b01c801d6ce4f9396a4cdf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 12 Apr 2012 17:17:58 +0200
Subject: [PATCH] new example from Why3 tutorial
---
mytest/MaxSum.scala | 50 +++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 50 insertions(+)
create mode 100644 mytest/MaxSum.scala
diff --git a/mytest/MaxSum.scala b/mytest/MaxSum.scala
new file mode 100644
index 000000000..6dc8d3b99
--- /dev/null
+++ b/mytest/MaxSum.scala
@@ -0,0 +1,50 @@
+import leon.Utils._
+
+object MaxSum {
+
+
+ def maxSum(a: Map[Int, Int], size: Int): (Int, Int) = ({
+ require(isArray(a, size) && size < 5 && isPositive(a, size))
+ var sum = 0
+ var max = 0
+ var i = 0
+ (while(i < size) {
+
+ if(max < a(i))
+ max = a(i)
+ sum + sum + a(i)
+ }) invariant (sum <= i * max)
+ (sum, max)
+ }) ensuring(res => res._1 <= size * res._2)
+
+ def isPositive(a: Map[Int, Int], size: Int): Boolean = {
+ require(size <= 10 && isArray(a, size))
+ def rec(i: Int): Boolean = {
+ require(i >= 0)
+ if(i >= size)
+ true
+ else {
+ if(a(i) < 0)
+ false
+ else
+ rec(i+1)
+ }
+ }
+ 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