Skip to content
Snippets Groups Projects
Commit 60f7ac7c authored by Mikaël Mayer's avatar Mikaël Mayer
Browse files

Added a verification testcases for testing conversion.

parent 9b8a691e
No related branches found
No related tags found
No related merge requests found
import leon.lang._
import leon.annotation._
import leon.collection._
import leon.collection.ListOps._
import leon.lang.synthesis._
object CompatibleListChar {
def rec[T](l : List[T], f : T => String): String = l match {
case Cons(head, tail) => f(head) + rec(tail, f)
case Nil() => ""
}
def customToString[T](l : List[T], p: List[Char], d: String, fd: String => String, fp: List[Char] => String, pf: String => List[Char], f : T => String): String = rec(l, f) ensuring {
(res : String) => (p == Nil[Char]() || d == "" || fd(d) == "" || fp(p) == "" || pf(d) == Nil[Char]()) && ((l, res) passes {
case Cons(a, Nil()) => f(a)
})
}
def customPatternMatching(s: String): Boolean = {
s match {
case "" => true
case b => List(b) match {
case Cons("", Nil()) => true
case Cons(s, Nil()) => false // StrOps.length(s) < BigInt(2) // || (s == "\u0000") //+ "a"
case Cons(_, Cons(_, Nil())) => true
case _ => false
}
case _ => false
}
} holds
}
\ No newline at end of file
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment