From 06b11bd6895d1c4b011f852f8ea88a0a299e08e2 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Tue, 19 Aug 2014 11:38:18 +0200
Subject: [PATCH] Add some simple examples of synthesis from examples, with
holes
---
testcases/synthesis/io-examples/Math.scala | 35 ++++++++++++++++++++++
1 file changed, 35 insertions(+)
create mode 100644 testcases/synthesis/io-examples/Math.scala
diff --git a/testcases/synthesis/io-examples/Math.scala b/testcases/synthesis/io-examples/Math.scala
new file mode 100644
index 000000000..df68735e3
--- /dev/null
+++ b/testcases/synthesis/io-examples/Math.scala
@@ -0,0 +1,35 @@
+import leon.lang._
+import leon.lang.synthesis._
+
+object Math {
+
+ def fib(a: Int): Int = {
+ require(a >= 0)
+ if (a > 1) {
+ fib(a-1) + fib(a-2)
+ } else {
+ ???[Int]
+ }
+ } ensuring {
+ passes(a, _)(Map(
+ 0 -> 0,
+ 1 -> 1,
+ 2 -> 1,
+ 3 -> 2,
+ 4 -> 3,
+ 5 -> 5,
+ 18 -> 2584
+ ))
+ }
+
+ def abs(a: Int): Int = {
+ if (?(a >= 0, a <= 0, a == 0, a != 0)) {
+ a
+ } else {
+ -a
+ }
+ } ensuring { _ >= 0 }
+
+
+
+}
--
GitLab