From 876217e4be8ac36fa0bc77de9a84ba2978a12dc4 Mon Sep 17 00:00:00 2001 From: Giuliano Losa <giuliano.losa@gmail.com> Date: Mon, 23 Aug 2010 15:50:57 +0000 Subject: [PATCH] --- vmcai2011-testcases/Giuliano.scala | 22 +++++++++++++++++++--- 1 file changed, 19 insertions(+), 3 deletions(-) diff --git a/vmcai2011-testcases/Giuliano.scala b/vmcai2011-testcases/Giuliano.scala index 99247ab24..51ed40b0a 100644 --- a/vmcai2011-testcases/Giuliano.scala +++ b/vmcai2011-testcases/Giuliano.scala @@ -5,10 +5,26 @@ object Giuliano { case class Cons(head: Int, tail: List) extends List case class Nil() extends List - def form1(x: Cons, y: Set[Int]) : Boolean = { - y.contains(x.head) && y.size == x.head - } ensuring(_ == true) + def f(x: Int) : Int = { throw new Exception("...") } + + def form1(x: Int, y: Set[Int]) : Boolean = { + // y.contains(x.head) && y.size == x.head + x != f(x) || f(x) == f(f(x)) + } // ensuring(_ == true) + def form2(f: Int, n: Int, servers: Set[Int], bizServers: Set[Int], corrServers: Set[Int], s: Set[Int]) : Boolean = { + require( + s.subsetOf(servers) + && s.size > f + && servers == corrServers ++ bizServers + && bizServers.size == f + && servers.size == n + && n > 3 + && f > 0 + && 3 * f < n + ) + (corrServers ** s).size >= 1 + } ensuring(_ == true) } // vim: set ts=4 sw=4 et: -- GitLab