From bee510e98ac382ecaa8520080ca8efbd5f6ccd69 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 13 Dec 2012 14:44:21 +0100
Subject: [PATCH] add euclidian division testcase for verification. Prove
validity
---
testcases/master-thesis-regis/Arithmetic.scala | 11 +++++++++++
1 file changed, 11 insertions(+)
diff --git a/testcases/master-thesis-regis/Arithmetic.scala b/testcases/master-thesis-regis/Arithmetic.scala
index 9173132e0..2b90bda91 100644
--- a/testcases/master-thesis-regis/Arithmetic.scala
+++ b/testcases/master-thesis-regis/Arithmetic.scala
@@ -70,4 +70,15 @@ object Arithmetic {
r
} ensuring(_ >= n)
+ def divide(x: Int, y: Int): (Int, Int) = {
+ require(x >= 0 && y > 0)
+ var r = x
+ var q = 0
+ (while(r >= y) {
+ r = r - y
+ q = q + 1
+ }) invariant(x == y*q + r && r >= 0)
+ (q, r)
+ } ensuring(res => x == y*res._1 + res._2 && res._2 >= 0 && res._2 < y)
+
}
--
GitLab