## Korat Tutorial

### Using Korat

Before writing your own examples and start generating new structures, keep in mind
that Korat requires:

- an
**imperative predicate**that specifies the desired structural constraints - a
**finitization**that bounds the desired test input size

#### Imperative predicate

Imperative predicate (also called repOK)
is a java method that checks class invariants.
Predicates don't take any parameters and should return
true for all valid structures and
false for all other. Korat uses this method
to check if the structure generated during the search is the valid one,
i.e. satisfies all class invariants and hence can be considered as a
valid test case. This means that every class you want to test using
Korat has to have its predicate method.

**Important**: it is a good practice to return false as soon as possible, before accessing all fields and checking all conditions. If a certain condition is not met, return false immediately, since that can speed up Korat search process significantly.

**Note**: when writing predicate methods you should always name them repOK because that is the default predicate name that Korat searches for. If you really want to use a different name, you can do that, but don't forget to inform Korat about it through the --predicate command line switch.#### Finitization

Finitization method tells Korat how to bound the input space.
The statements in the finitization method specify bounds on the
number of objects to be used to construct instances of the data structure, as well
as possible values stored in the fields of those objects. The basic idea is to
create

*Field domains*for all fields that you want Korat to vary during the search process. Each field domain will contain a set of values that its corresponding field can take during the search. For reference type fields we call them*ObjSet*and for primitive types we have*IntSet*,*FloatSet*and so on. In general, it is perfectly fine to have single field domain associated with many fields.

**Note**: when writing finitization methods you should always name them fin<className> because that is the default finitization name that Korat searches for. If you really want to use a different name, you can do that, but don't forget to inform Korat about it through the --finitization command line switch.The rest of this section will help you better understand these two concepts by going through BinaryTree and HeapArray examples and explaining them in more detail. After reading this tutorial, you should be able to easily write finitization and predicate methods for your own structures.

### BinaryTree Example

#### Introduction

This example illustrates the generation and checking of linked data structures using simple binary trees. Each tree node has pointers to its left and right child and binary tree itself has a pointer to the root node and an int value that says the number of all nodes in the tree. Skeleton for this structure could look like:public class BinaryTree { public static class Node { Node left; Node right; } private Node root; private int size; }

#### Writing predicate method (repOK)

Now we want to write a predicate method. In the case of binary trees,
predicate method checks that the tree doesn't have any cycles and that
the number of nodes traversed from root matches the value of the field
size. Simple method like the following
should do the job. Note that it returns false as soon as it can.

public boolean repOK() { if (root == null) return size == 0; // checks that tree has no cycle Set visited = new HashSet(); visited.add(root); LinkedList workList = new LinkedList(); workList.add(root); while (!workList.isEmpty()) { Node current = (Node) workList.removeFirst(); if (current.left != null) { if (!visited.add(current.left)) return false; workList.add(current.left); } if (current.right != null) { if (!visited.add(current.right)) return false; workList.add(current.right); } } // checks that size is consistent return (visited.size() == size); }

#### Writing finitization method (finBinaryTree)

The only thing that's left to be done is to tell
Korat how to bound the input space.

public static IFinitization finBinaryTree(int nodesNum, int minSize, int maxSize) { IFinitization f = FinitizationFactory.create(BinaryTree.class); IObjSet nodes = f.createObjSet(Node.class, nodesNum, true); f.set("root", nodes); f.set("Node.left", nodes); f.set("Node.right", nodes); IIntSet sizes = f.createIntSet(minSize, maxSize); f.set("size", sizes); return f; }

Here is the explanation line-by-line.

First line just creates an "empty" finitization using
FinitizationFactory.create factory method by passing it
class under test as an argument.

Then, a set of nodes is created by calling
createObjSet method.
This method takes several parameters:

- class of objects to be created
- number of objects of the given class to be created
- whether to include null or not

Next thing to do is to associate certain fields with newly created object set.
Fields BinaryTree.root, Node.left
and Node.right are all of type Node
and it is ok to have them all associated with this object set. That is what next three lines
do.

Only field that is left to be bounded is BinaryTree.size
so we simply create an IntSet and assign it to the field
size.

### HeapArray Example

#### Introduction

This example illustrates the generation and checking of array-based
data structures, using the heap data structure. The (binary) heap
data structure can be viewed as a complete binary tree ā the tree is
completely filled on all levels except possibly the lowest, which is
filled from the left up to some point. Heaps also satisfy the heap
property ā for every node n other than the root, the value of nās
parent is greater than or equal to the value of n. Heap structure can be
efficiently implemented using a single array to represent all heap nodes.
Skeleton for this implementation could look like:

public class HeapArray { private int size; private int array[]; }

#### Writing predicate method (repOK)

Predicate method should check that all heap properties are satisfied. It returns false as soon as possible, immediately after discovers that some conditions are not met.public boolean repOK() { if (array == null) return false; if (size < 0 || size > array.length) return false; for (int i = 0; i < size; i++) { int elem_i = array[i]; if (elem_i == -1) return false; if (i > 0) { int elem_parent = array[(i - 1) / 2]; if (elem_i > elem_parent) return false; } } for (int i = size; i < array.length; i++) if (array[i] != -1) return false; return true; }

#### Writing finitization method (finHeapArray)

Finitization method looks basically the same as the finitization for
the BinaryTree example, so you should first take a look into the previous
example if haven't already done so. A single new thing here is the finitization of
arrays.

public static IFinitization finHeapArray(int maxSize, int maxArrayLength, int maxArrayValue) { IFinitization f = FinitizationFactory.create(HeapArray.class); IIntSet sizes = f.createIntSet(0, 1, maxSize); IIntSet arrayLength = f.createIntSet(0, 1, maxArrayLength); IIntSet arrayValues = f.createIntSet(-1, 1, maxArrayValue); IArraySet arrays = f.createArraySet(int[].class, arrayLength, arrayValues, 1); f.set("size", sizes); f.set("array", arrays); return f; }

To finitize array fields, you must provide two field domains. First one
(arrayLength in the code above) is
IIntSet which tells all possible values that
array length can take. The second one (arrayValues
in the code above) tells all possible values that array elements can take.
This field domain has to be compatible with the array type, meaning that
in the case of int arrays (like in this example) it has to be
IIntSet and in the case of reference type arrays
it has to be IObjSet with appropriate class of objects.