From 2f62cb9810dca94b221d90e1b7dade96b497c6b7 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Mon, 30 Jun 2014 18:13:57 +0200
Subject: [PATCH] more xlang max sum testcases
---
testcases/xlang/MaxSum.scala | 23 +++++++++++++++++++++++
1 file changed, 23 insertions(+)
diff --git a/testcases/xlang/MaxSum.scala b/testcases/xlang/MaxSum.scala
index 3d414f397..f4d056ab9 100644
--- a/testcases/xlang/MaxSum.scala
+++ b/testcases/xlang/MaxSum.scala
@@ -35,4 +35,27 @@ object MaxSum {
rec(0)
}
+ def summ(to : Int): Int = ({
+ require(to >= 0)
+ var i = 0
+ var s = 0
+ (while (i < to) {
+ s = s + i
+ i = i + 1
+ }) invariant (s >= 0 && i >= 0 && s == i*(i-1)/2 && i <= to)
+ s
+ }) ensuring(res => res >= 0 && res == to*(to-1)/2)
+
+
+ def sumsq(to : Int): Int = ({
+ require(to >= 0)
+ var i = 0
+ var s = 0
+ (while (i < to) {
+ s = s + i*i
+ i = i + 1
+ }) invariant (s >= 0 && i >= 0 && s == (i-1)*i*(2*i-1)/6 && i <= to)
+ s
+ }) ensuring(res => res >= 0 && res == (to-1)*to*(2*to-1)/6)
+
}
--
GitLab