From 32e07b6cb4bf5706a960ddfac33797df2a4f9e4a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ali=20Sinan=20K=C3=B6ksal?= <alisinan@gmail.com>
Date: Wed, 23 Feb 2011 10:32:01 +0000
Subject: [PATCH] The sketched squaring function is indeed valid.
---
clp/IntSynth.scala | 6 ++++++
1 file changed, 6 insertions(+)
diff --git a/clp/IntSynth.scala b/clp/IntSynth.scala
index f4ea0bd79..6113da1ef 100644
--- a/clp/IntSynth.scala
+++ b/clp/IntSynth.scala
@@ -41,6 +41,12 @@ object IntSynth {
mySquare(5,q1,q2,q3)==25)
} holds
+ def mySquareSketched(x : Int) : Int = {
+ require (x >= 0)
+ if (x <= 1) x
+ else 4 * x + mySquareSketched(x - 2) - 4
+ } ensuring(res => specSqr(x, res))
+
//def gotThis(x : Int) = mySquare(x, 0, 4, -4)
//println(gotThis(10)) --> 100
}
--
GitLab