Korat - Tutorial

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

which means that the second line creates a set of Node objects which contain null plus nodesNum instances of class Node.

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.