From a8a18953839fffb6d4b189a603894f3afd95267b Mon Sep 17 00:00:00 2001 From: Viktor Kuncak <vkuncak@gmail.com> Date: Tue, 31 May 2011 20:02:59 +0000 Subject: [PATCH] one can use lemmas by conjoining their instances --- testcases/RedBlackTree.scala | 5 +++++ testcases/UseContradictoryLemma.scala | 15 +++++++++++++++ 2 files changed, 20 insertions(+) create mode 100644 testcases/UseContradictoryLemma.scala diff --git a/testcases/RedBlackTree.scala b/testcases/RedBlackTree.scala index 70f3d6316..0952a11fe 100644 --- a/testcases/RedBlackTree.scala +++ b/testcases/RedBlackTree.scala @@ -51,4 +51,9 @@ object RedBlackTree { case Node(Red(),l,v,r) => Node(Black(),l,v,r) case _ => n } + + def flip(t : Tree) : Tree = t match { + case Empty() => Empty() + case Node(color,l,e,r) => Node(color,flip(r),e,flip(l)) + } } diff --git a/testcases/UseContradictoryLemma.scala b/testcases/UseContradictoryLemma.scala new file mode 100644 index 000000000..f25cec124 --- /dev/null +++ b/testcases/UseContradictoryLemma.scala @@ -0,0 +1,15 @@ +import scala.collection.immutable.Set +import funcheck.Utils._ +import funcheck.Annotations._ + +object UseContradictoryLemma { + + def lemma1(x : Int) : Boolean = { + x == 1 + } holds + + def f(x : Int) : Int = { + 5 + } ensuring (x => lemma1(x) && x == 1) + +} -- GitLab