diff --git a/clp/IntSynth.scala b/clp/IntSynth.scala index f4ea0bd791bea62d838ebb586fa27fde551ddba1..6113da1ef67cc27198e09b3e3755fbbee915a9c7 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 }