Skip to content
Snippets Groups Projects
Commit c23d1da1 authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

Better spec for find

parent 2939be54
No related branches found
No related tags found
No related merge requests found
...@@ -223,7 +223,7 @@ sealed abstract class List[T] { ...@@ -223,7 +223,7 @@ sealed abstract class List[T] {
case Some(i) => Some(i+1) case Some(i) => Some(i+1)
} }
} }
}} ensuring { _.isDefined == this.contains(e) } }} ensuring { res => !res.isDefined || (this.content contains e) }
def init: List[T] = { def init: List[T] = {
require(!isEmpty) require(!isEmpty)
...@@ -410,7 +410,7 @@ sealed abstract class List[T] { ...@@ -410,7 +410,7 @@ sealed abstract class List[T] {
case Nil() => None[T]() case Nil() => None[T]()
case Cons(h, t) if p(h) => Some(h) case Cons(h, t) if p(h) => Some(h)
case Cons(_, t) => t.find(p) case Cons(_, t) => t.find(p)
}} ensuring { _.isDefined == exists(p) } }} ensuring { res => !res.isDefined || content.contains(res.get) }
def groupBy[R](f: T => R): Map[R, List[T]] = this match { def groupBy[R](f: T => R): Map[R, List[T]] = this match {
case Nil() => Map.empty[R, List[T]] case Nil() => Map.empty[R, List[T]]
......
...@@ -19,9 +19,11 @@ sealed abstract class Option[T] { ...@@ -19,9 +19,11 @@ sealed abstract class Option[T] {
case None() => default case None() => default
} }
def orElse(or: Option[T]) = this match { def orElse(or: Option[T]) = {this match {
case Some(v) => this case Some(v) => this
case None() => or case None() => or
}} ensuring {
res => (this.isDefined || or.isDefined) == res.isDefined
} }
def isEmpty = this match { def isEmpty = this match {
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment