From 4bb9f4cc6c3990e67322284afd2e9ebe3f021068 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 16 Dec 2015 17:50:46 +0100
Subject: [PATCH] Fix drop example
---
testcases/repair/List/List13.scala | 24 ++++++++++++++++--------
1 file changed, 16 insertions(+), 8 deletions(-)
diff --git a/testcases/repair/List/List13.scala b/testcases/repair/List/List13.scala
index 914f0caac..1093efc3d 100644
--- a/testcases/repair/List/List13.scala
+++ b/testcases/repair/List/List13.scala
@@ -78,14 +78,22 @@ sealed abstract class List[T] {
}
}
- def drop(i: BigInt): List[T] = (this, i) match {
- case (Nil(), _) => Nil()
- case (Cons(h, t), i) =>
- if (i == 0) {
- Cons(h, t)
- } else {
- t.drop(i) // FIXME Should be -1
- }
+ def drop(i: BigInt): List[T] = {
+ require(i >= 0)
+ (this, i) match {
+ case (Nil(), _) => Nil[T]()
+ case (Cons(h, t), i) =>
+ if (i == 0) {
+ Cons[T](h, t)
+ } else {
+ t.drop(i) // FIXME Should be -1
+ }
+ }
+ } ensuring { (res: List[T]) =>
+ ((this, i), res) passes {
+ case (Cons(a, Cons(b, Nil())), BigInt(1)) => Cons(b, Nil())
+ case (Cons(a, Cons(b, Nil())), BigInt(2)) => Nil()
+ }
}
def slice(from: BigInt, to: BigInt): List[T] = {
--
GitLab