Scaludita Examples

Scaludita is based on Udita system but adapted to Scala by Tihomir Gvero

Finding a Solution of Simple Constraint

```  def assume(p : Boolean) = Verify.ignoreIf(!p)
def choose = Verify.getInt(1,20)

val y = 11
val x = choose
assume(10 < y && x < 5 && y < 3*x)
println("x = " + x)```

Structural Constraints: Red-Black Tree Implementation

```package redblacktree

import gov.nasa.jpf.jvm.Verify;
import gov.nasa.jpf.jvm.generators.StructureCounter;

object RedBlackTreeTest extends Application {
val MAXTREESIZE = 4

abstract class Color
case class RED extends Color
case class BLACK extends Color

sealed abstract class Tree
case class Empty extends Tree
case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree

def member(x: Int, t:Tree): Boolean = t match {
case Empty() => false
case Node(_,a,y,b) =>
if (x < y) member(x,a)
else if (x > y) member(x,b)
else true
}

def insert(x: Int, t: Tree): Tree = {
def ins(t: Tree): Tree = t match {
case Empty() => Node(RED(),Empty(),x,Empty())
case Node(c,a,y,b) =>
if      (x < y)  balance(c, ins(a), y, b)
else if (x == y) Node(c,a,y,b)
else             // balance(c,a,y,ins(b))
Node(c,a,y,ins(b))
}
makeBlack(ins(t))
}

def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = (c,a,x,b) match {
case (BLACK(),Node(RED(),Node(RED(),a,xV,b),yV,c),zV,d) =>
Node(RED(),Node(BLACK(),a,xV,b),yV,Node(BLACK(),c,zV,d))
case (BLACK(),Node(RED(),a,xV,Node(RED(),b,yV,c)),zV,d) =>
Node(RED(),Node(BLACK(),a,xV,b),yV,Node(BLACK(),c,zV,d))
case (BLACK(),a,xV,Node(RED(),Node(RED(),b,yV,c),zV,d)) =>
Node(RED(),Node(BLACK(),a,xV,b),yV,Node(BLACK(),c,zV,d))
case (BLACK(),a,xV,Node(RED(),b,yV,Node(RED(),c,zV,d))) =>
Node(RED(),Node(BLACK(),a,xV,b),yV,Node(BLACK(),c,zV,d))
case (c,a,xV,b) => Node(c,a,xV,b)
}

/** makeBLACK: Turn a node BLACK. */
def makeBlack(n: Tree): Tree = n match {
case Node(RED(),l,v,r) => Node(BLACK(),l,v,r)
case _ => n
}

/* global invariants:
* RED-BLACK trees are binary search trees obeying two key invariants:
*
* (1) Any path from a root node to a leaf node contains the same number
*     of BLACK nodes. (A balancing condition.)
*
* (2) RED nodes always have BLACK children.
*
*/

/* Empty tree are consideRED to be BLACK */
def isBLACK(t: Tree): Boolean = t match {
case Node(RED(),_,_,_) => false
case _ => true
}

private def getSubTree(size:Int, min:Int, max:Int): Tree = {
if (size == 0) Empty()
else if (size == 1)
Node(if (Verify.getBoolean()) RED()
else BLACK(), Empty(), Verify.getInt(min,max), Empty())
else {
val value = Verify.getInt(min,max)
val leftSize = value - min
val rightSize = size - 1 - leftSize
Node(if (Verify.getBoolean()) RED() else BLACK(),
getSubTree(leftSize, min, value - 1), value, getSubTree(rightSize, value + 1, max))
}
}

private def generateBinarySearchTree(treeSize:Int): Tree = {
val size = Verify.getInt(1, treeSize)
val maxNodeValue = size - 1
val t = getSubTree(size, 0, maxNodeValue)
t
}

// declarative, naive representation
def anyPathsContainsSameNumberOfBlackNodes(t: Tree): Boolean = {
def blackNodeNos(t: Tree, acc: Int): List[Int] = t match {
case Empty() => List(acc + 1) // because Empty are assumed to be BLACK
case Node(_,l,_,r) => {
val upAcc = if(isBLACK(t)) acc + 1 else acc
blackNodeNos(l,upAcc) ::: blackNodeNos(r,upAcc) }
}
val paths = blackNodeNos(t, 0)

}

def areRedNodeChildrenBlack(t: Tree): Boolean = t match {
case Node(RED(),l,_,r) =>
isBLACK(l) && isBLACK(r) &&
areRedNodeChildrenBlack(l) && areRedNodeChildrenBlack(r)
case Node(BLACK(),l,_,r) =>
areRedNodeChildrenBlack(l) && areRedNodeChildrenBlack(r)
case _ => true
}

def generateRedBlackTree(treeSize:Int): Tree = {
val t = generateBinarySearchTree(treeSize)
t
}

def content(t:Tree):Set[Int] = t match {
case Empty() => Set.empty
case Node(_,left,value,right) => (content(left) ++ Set(value) ++ content(right))
}

def forAllrbt(property: (Tree,Int) => Boolean){
val size = Verify.getInt(1,MAXTREESIZE+1)
val t = generateRedBlackTree(size)
val x = Verify.getInt(0,size)
val prop = property(t,x)
StructureCounter.incCounters(prop)
if (!prop) {
System.out.println("____________________________________________________________________")
System.out.println("| Found counterexample: " + t+" "+x)
System.out.println("--------------------------------------------------------------------")
assert(false)
}
//System.out.println(t+" "+x)
}

forAllrbt((t:Tree, x:Int)  => ({
val t1 = insert(x,t)