From be2021c8b3cbd29ffdd286b076d112c2eae79940 Mon Sep 17 00:00:00 2001
From: Mirco Dotta <mirco.dotta@gmail.com>
Date: Mon, 13 Jul 2009 15:02:03 +0000
Subject: [PATCH] Added new properties to verify.
---
tests/plugin/ConsSnoc.scala | 67 ++++++++++++++++++-------------------
1 file changed, 33 insertions(+), 34 deletions(-)
diff --git a/tests/plugin/ConsSnoc.scala b/tests/plugin/ConsSnoc.scala
index aaf6bed75..017347d28 100644
--- a/tests/plugin/ConsSnoc.scala
+++ b/tests/plugin/ConsSnoc.scala
@@ -9,7 +9,7 @@ object ConsSnoc {
/* Class Hierarchy */
@generator
sealed abstract class Lst
- class Cons(val head: Int, val tail: Lst) extends Lst
+ class Cons(val head: Int, val tail: Lst) extends Lst
class Nill extends Lst
@@ -44,20 +44,6 @@ object ConsSnoc {
}
}
}
-
- /*
- object Snoc {
- def unapply(c: Cons): Option[(Lst,Int)] = c match {
- case Cons(c, xs) => xs match {
- case Nill() => Some((Nill(),c))
- case Snoc(ys, y) => Some((Cons(c,ys),y))
- }
- }
- }
- */
-
-
-
def firstAndLast(lst: Lst): Lst = lst match {
case Nill() => lst
@@ -67,31 +53,44 @@ object ConsSnoc {
def main(args: Array[String]) = {}
- /* domain
- Dom_Nill = Nill &
- Dom_Cons = Cons &
- Dom_Snoc = Cons &
- Dom_Cons \Un Dom_Nill = Lst &
- Dom_Cons \Int Dom_Nill = empty
- */
- forAll{n: Nill => Nill.unapply(n)} // Dom_Nill = Nill
- forAll{c: Cons => Cons.unapply(c).isDefined} // Dom_Cons = Cons
- forAll{c: Cons => Snoc.unapply(c).isDefined} // Dom_Snoc = Cons
+
+ // Nill extractor always succeed for Nill instances
+ forAll{n: Nill => Nill.unapply(n)}
+ // Cons extractor always succeed for Cons instances
+ forAll{c: Cons => Cons.unapply(c).isDefined}
+ // Cons extractor succeed iff the passed object instance is of type Cons
+ forAll{l: Lst => Cons.unapply(l).isEmpty || (Cons.unapply(l).isDefined && l.isInstanceOf[Cons]) }
+ // Snoc extractor always succeed for Cons instances
+ forAll{c: Cons => Snoc.unapply(c).isDefined}
+ // Snoc extractor succeed iff the passed object instance is of type Cons
+ forAll{l: Lst => Cons.unapply(l).isEmpty || (Snoc.unapply(l).isDefined && l.isInstanceOf[Cons])}
+
+ /* These are postconditions, but they are checked as program axioms */
+ // Check behavior of Cons extractor
+ forAll{c: Cons => equalLst(cons(Cons.unapply(c).get), c)}
+ // Check behavior of Snoc extractor
+ forAll{c: Cons => equalLst(concat(Snoc.unapply(c).get), c) }
// partition
- forAll{l: Lst => Cons.unapply(l).isDefined || Nill.unapply(l)} // Dom_Cons \Un Dom_Nill = Lst
- forAll{l: Lst => !(Cons.unapply(l).isDefined && Nill.unapply(l))} //Dom_Cons \Int Dom_Nill = empty
+ // For any Lst, either the Cons or the Nill extractor applies
+ forAll{l: Lst => Cons.unapply(l).isDefined || Nill.unapply(l)}
+ // For any Lst, it is never the case that both the Cons and the Nill extractor applies
+ forAll{l: Lst => !(Cons.unapply(l).isDefined && Nill.unapply(l))}
// the two above properties could be simmply be written as
//forAll{l: Lst => Cons.unapply(l).isDefined ^^ Nill.unapply(l)}
- /* axioms */
- forAll[(Int,Lst)]{ p => equalCons(Cons.unapply(Cons(p._1,p._2)), Some(p._1,p._2))}
+ /* list axioms */
+ forAll[(Int,Cons)]{ p => (Cons.unapply(Cons(p._1,p._2)).get._1 == p._1) &&
+ equalLst(Cons.unapply(Cons(p._1,p._2)).get._2, p._2) }
+ forAll[(Int, Cons)] { p => Cons(p._1,p._2).head == p._1}
+ forAll[(Int, Cons)] { p => Cons(p._1,p._2).tail == p._2}
- def equalCons(p1: Option[(Int,Lst)], p2: Option[(Int,Lst)]): Boolean = (p1,p2) match {
- case (None,None) => true
- case (Some((x,xs)), Some((y,ys))) =>
- equalLst(Cons(x,xs),Cons(y,ys))
- case _ => false
+
+ def cons(s: (Int,Lst)): Cons = Cons(s._1, s._2)
+
+ def concat(c: (Lst, Int)): Lst = c._1 match {
+ case Nill() => Cons(c._2, Nill())
+ case Cons(x,xs) => Cons(x,concat(xs,c._2))
}
def equalLst(l1: Lst, l2: Lst): Boolean = (l1,l2) match {
--
GitLab