Features

Contents

1. Function Evaluation
2. Searching For Inputs
3. Computing With Sets
4. Generating Test Inputs

Function Evaluation

Zen can execute the function we have built on a given collection of inputs. The simplest way to do so is to call the Evaluate method on the ZenFunction:

Zen<int> MultiplyAndAdd(Zen<int> x, Zen<int> y)
{
    return 3 * x + y;
}

...

ZenFunction<int, int, int> function = Function<int, int, int>(MultiplyAndAdd);
var output = function.Evaluate(3, 2); // output = 11

This will interpret abstract syntax tree represented by the Zen function at runtime. Of course doing so can be quite slow, particularly compared to a native version of the function.

When performance is important, or if you need to execute the model on many inputs, Zen can compile the model using the C# System.Reflection.Emit API. This generates IL instructions that execute more efficiently. Doing so is easy, just call the Compile method on the function first:

function.Compile();
output = function.Evaluate(3, 2); // output = 11

We can see the difference by comparing the performance between the two:

var watch = System.Diagnostics.Stopwatch.StartNew();

for (int i = 0; i < 1000000; i++)
    function.Evaluate(3, 2);

Console.WriteLine($"interpreted function time: {watch.ElapsedMilliseconds}ms");
watch.Restart();

function.Compile();

Console.WriteLine($"compilation time: {watch.ElapsedMilliseconds}ms");
watch.Restart();

for (int i = 0; i < 1000000; i++)
    function.Evaluate(3, 2);

Console.WriteLine($"compiled function time: {watch.ElapsedMilliseconds}ms");

interpreted function time: 4601ms
compilation time: 4ms
compiled function time: 2ms

Searching For Inputs

A powerful feature Zen supports is the ability to find function inputs that lead to some (un)desirable outcome. For example, we can find an (x, y) input pair such that x is less than zero and the output of the function is 11:

var input = function.Find((x, y, result) => And(x <= 0, result == 11)); 
// input.Value = (-1883171776, 1354548043)

The type of the result in this case is Option<(int, int)>, which will have a pair of integer inputs that make the expression true if such a pair exists. In this case the library will find x = -1883171776 and y = 1354548043

To find multiple inputs, Zen supports an equivalent FindAll method, which returns an IEnumerable of inputs.

var inputs = function.FindAll((x, y, result) => And(x <= 0, result == 11)).Take(5);

Each input in inputs will be unique so there will be no duplicates.

Zen also supports richer data types such as lists. For example, we can write an implementation for the insertion sort algorithm using recursion:

Zen<IList<T>> Sort<T>(Zen<IList<T>> expr)
{
    return expr.Case(empty: EmptyList<T>(), cons: (hd, tl) => Insert(hd, Sort(tl)));
}

Zen<IList<T>> Insert<T>(Zen<T> elt, Zen<IList<T>> list)
{
    return list.Case(
        empty: Singleton(elt),
        cons: (hd, tl) => If(elt <= hd, list.AddFront(elt), Insert(elt, tl).AddFront(hd)));
}

We can verify properties about this sorting algorithm by proving that there is no input that can lead to some undesirable outcome. For instance, we can use Zen to show that a sorted list has the same length as the input list:

var f = Function<IList<byte>, IList<byte>>(l => Sort(l));
var input = f.Find((inlist, outlist) => inlist.Length() != outlist.Length());
// input = None

Input search uses bounded model checking to perform verification. For data structures like lists, it finds examples up to a given input size k, which is an optional parameter to the function.

Computing With Sets

While the Find function provides a way to find a single input to a function, Zen also provides an additional API for reasoning about sets of inputs and outputs to functions.

It does this through a StateSetTransformer API. A transformer is created by calling the Transformer() method on a ZenFunction:

ZenFunction<uint, uint> f = Function<uint, uint>(i => i + 1);

// create a set transformer from the function
StateSetTransformer<uint, uint> t = f.Transformer();

Transformers allow for manipulating (potentially huge) sets of objects efficient. For example, we can get the set of all input uint values where adding one will result in an output y that is no more than 10 thousand:

// find the set of all inputs where the output is no more than 10,000
StateSet<uint> inputSet = t.InputSet((x, y) => y <= 10000);

This set will include all the values 0 - 9999 as well as uint.MaxValue due to wrapping. Transformers can also manpulate sets by propagating them forward or backwards:

// run the set through the transformer to get the set of all outputs
StateSet<uint> outputSet = t.TransformForward(inputSet);

Finally, StateSet objects can also be intersected, unioned, and negated. We can pull an example element out of a set as follows:

// get an example value in the set if one exists.
Option<uint> example = inputSet.Element(); // example.Value = 0

Internally, transformers leverage binary decision diagrams to represent, possibly very large, sets of objects efficiently.

Generating Test Inputs

As a final use case, Zen can automatically generate interesting use cases for a given model by finding inputs that will lead to different execution paths. For instance, consider again the insertion sort implementation. We can ask Zen to generate test inputs for the function that can then be used, for instance to test other sorting algorithms:

var f = Function<IList<byte>, IList<byte>>(l => Sort(l));

foreach (var list in f.GenerateInputs(listSize: 3))
{
    Console.WriteLine($"[{string.Join(",", list)}]");
}

In this case, we get the following output, which includes all permutations of relative orderings that may affect a sorting algorithm.

[]
[0]
[0,0]
[0,0,0]
[64,54]
[0,64,54]
[136,102,242]
[32,64,30]
[136,103,118]
[144,111,14]

The test generation approach uses symbolic execution to enumerate program paths and solve constraints on inputs that lead down each path.