From 7a316cb10097bfa5b9234243a3ee7ab7ed7cfb55 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 12 Apr 2012 18:41:33 +0200
Subject: [PATCH] more examples
---
mytest/Add.scala | 25 +++++++++++++++++++++++++
mytest/Bubble.scala | 2 ++
mytest/LinearSearch.scala | 2 ++
mytest/MaxSum.scala | 28 ++++++++++++++++++++++++----
mytest/Mult.scala | 26 ++++++++++++++++++++++++++
5 files changed, 79 insertions(+), 4 deletions(-)
create mode 100644 mytest/Add.scala
create mode 100644 mytest/Mult.scala
diff --git a/mytest/Add.scala b/mytest/Add.scala
new file mode 100644
index 000000000..5d125e3c7
--- /dev/null
+++ b/mytest/Add.scala
@@ -0,0 +1,25 @@
+import leon.Utils._
+
+/* VSTTE 2008 - Dafny paper */
+
+object Add {
+
+ def add(x : Int, y : Int): Int = ({
+ var r = x
+ if(y < 0) {
+ var n = y
+ (while(n != 0) {
+ r = r - 1
+ n = n + 1
+ }) invariant(r == x + y - n && 0 <= -n)
+ } else {
+ var n = y
+ (while(n != 0) {
+ r = r + 1
+ n = n - 1
+ }) invariant(r == x + y - n && 0 <= n)
+ }
+ r
+ }) ensuring(_ == x+y)
+
+}
diff --git a/mytest/Bubble.scala b/mytest/Bubble.scala
index 4312fed85..33ad5c103 100644
--- a/mytest/Bubble.scala
+++ b/mytest/Bubble.scala
@@ -1,5 +1,7 @@
import leon.Utils._
+/* The calculus of Computation textbook */
+
object Bubble {
def sort(a: Map[Int, Int], size: Int): Map[Int, Int] = ({
diff --git a/mytest/LinearSearch.scala b/mytest/LinearSearch.scala
index 35e7cb300..e91a3f267 100644
--- a/mytest/LinearSearch.scala
+++ b/mytest/LinearSearch.scala
@@ -1,5 +1,7 @@
import leon.Utils._
+/* The calculus of Computation textbook */
+
object LinearSearch {
def linearSearch(a: Map[Int, Int], size: Int, c: Int): Boolean = ({
diff --git a/mytest/MaxSum.scala b/mytest/MaxSum.scala
index 6dc8d3b99..07c5d12ab 100644
--- a/mytest/MaxSum.scala
+++ b/mytest/MaxSum.scala
@@ -1,5 +1,7 @@
import leon.Utils._
+/* VSTTE 2010 challenge 1 */
+
object MaxSum {
@@ -9,16 +11,34 @@ object MaxSum {
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 = sum + a(i)
+ i = i + 1
+ }) invariant (sum <= i * max && /*isGreaterEq(a, i, max) &&*/ /*(if(i == 0) max == 0 else true) &&*/ i >= 0 && i <= size)
(sum, max)
}) ensuring(res => res._1 <= size * res._2)
+/*
+ def isGreaterEq(a: Map[Int, Int], size: Int, n: Int): Boolean = {
+ require(size <= 5 && isArray(a, size))
+ def rec(i: Int): Boolean = {
+ require(i >= 0)
+ if(i >= size)
+ true
+ else {
+ if(a(i) > n)
+ false
+ else
+ rec(i+1)
+ }
+ }
+ rec(0)
+ }
+ */
+
def isPositive(a: Map[Int, Int], size: Int): Boolean = {
- require(size <= 10 && isArray(a, size))
+ require(size <= 5 && isArray(a, size))
def rec(i: Int): Boolean = {
require(i >= 0)
if(i >= size)
diff --git a/mytest/Mult.scala b/mytest/Mult.scala
new file mode 100644
index 000000000..417e9e9cd
--- /dev/null
+++ b/mytest/Mult.scala
@@ -0,0 +1,26 @@
+import leon.Utils._
+
+/* VSTTE 2008 - Dafny paper */
+
+object Mult {
+
+ def mult(x : Int, y : Int): Int = ({
+ var r = 0
+ if(y < 0) {
+ var n = y
+ (while(n != 0) {
+ r = r - x
+ n = n + 1
+ }) invariant(r == x * (y - n) && 0 <= -n)
+ } else {
+ var n = y
+ (while(n != 0) {
+ r = r + x
+ n = n - 1
+ }) invariant(r == x * (y - n) && 0 <= n)
+ }
+ r
+ }) ensuring(_ == x*y)
+
+}
+
--
GitLab