From 5fb6c7d67dd2fb3a96646c9ef3d0a6ca147dc2b1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ali=20Sinan=20K=C3=B6ksal?= <alisinan@gmail.com>
Date: Thu, 18 Nov 2010 15:29:29 +0000
Subject: [PATCH] inductive proof for size of append.
---
testcases/ListWithSize.scala | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/testcases/ListWithSize.scala b/testcases/ListWithSize.scala
index 4e3be387f..a69deb6fb 100644
--- a/testcases/ListWithSize.scala
+++ b/testcases/ListWithSize.scala
@@ -72,6 +72,10 @@ object ListWithSize {
case Cons(x,xs) => sizeAppend(xs, l2)
}) ensuring(res => res && size(append(l1,l2)) == size(l1) + size(l2))
+ @induct
+ def sizeAppendInductive(l1 : List, l2 : List) : Boolean =
+ (size(append(l1, l2)) == size(l1) + size(l2)) holds
+
// proved with unrolling=4
def concat(l1: List, l2: List) : List = concat0(l1, l2, Nil())
// ensuring(content(_) == content(l1) ++ content(l2))
--
GitLab