Axioms-only tutorial

In this tutorial, we introduce the automated testing utilities of Catsfoot for people who are not interested in concepts, or just not familiar enough with C++ templates.


Let's say we have the following implementation of integer exponentiation.

unsigned long
pow(unsigned long b,
    unsigned short e) {
  if (e == 0)
    return 1;
  auto rec = pow(b, e/2);
  return ((e%2)?b:1)*rec*rec;

Axioms are defined as C++ functions containing assertions, possibly conditional. Nevertheless, the user is free to write any kind of code.

If we wanted to test Fermat's theorem on native unsigned integers with the definition of pow, we could write an axiom like this:

fermat(unsigned long x, unsigned long y, unsigned long z,
       unsigned short n) {
  if ((n > 2) && (x > 0) && (y > 0))
    axiom_assert(pow(x, n) + pow(y, n) != pow(z, n));

The assertion is probably actually not true in case of overflow. We will try to investigate if it fails, and how.


We want to generate data for the axiom. We need two types of values: unsigned long and unsigned short. One way is to give lists of values.

simple_test() {
  auto generator =
    list_data_generator<unsigned long, unsigned short>(
      {1ul, 2ul, 3ul, 4ul, 5ul, 6ul},
      {3ul, 4ul, 5ul, 6ul});

  if (!test(generator, fermat, "fermat"))
    return false;

  return true;

The test itself will print information in the error output. It will return true on success. It is then possible build a test suite and directly call the function.

The test will pass here. It does because it is not intensively testing the axiom. If we used random numbers, we would likely eventually discover that for some special values, an overflow will appear to put zeroes in the factors of the exponentiation. Thus, the return value is zero.

We can write a test using random. And we will find that some values break the axiom.

random_test(std::mt19937& engine) {
  auto generator =
    term_generator_builder<unsigned long, unsigned short>(10u)
     std::function<unsigned long()>
     ([&engine] () {
       return std::uniform_int_distribution<unsigned long>()(engine);
     std::function<unsigned short()>
     ([&engine] () {
       return std::uniform_int_distribution<unsigned short>()(engine);

The output will give us some information like: Axiom void fermat(long unsigned int, long unsigned int, long unsigned int, short unsigned int) failed.

Expression was: pow(x, n) + pow(y, n) != pow(z, n)

Values were:
 * 12775342532353695410
 * 12775342532353695410
 * 8564872738844034446
 * 23302

Random generation of integers is not interesting for the purposes of the tutorial, and so we do not explain the example in detail. Basically we give two functions generating two different types.

Term generators

We can now start with a new example. We will use an example from Haskell's Quickcheck. The example is a function taking a stream as input and returning a list of the first five characters which are in range from 'a' to 'e'.

std::string getList(std::istream& input) {
  std::string ret = "";
  unsigned count = 0;
  char c;
  while (input >> c) {
    if ((c >= 'a') && (c <= 'e')) {
      if (++count >= 5)
        return ret;
  return ret;

We can now write an axiom verifying that the list is never longer than 5 characters. We can also check that all the contained characters are actually from the valid range. We can make several assertions in the same axiom.

void axiom(std::istream& s) {
  std::string str = getList(s);
  axiom_assert(str.length() <= 5);
  for (auto c : str) {
    axiom_assert((c >= 'a') && (c <= 'e'));

Now we can start to write our test. Generating random strings works well with term generation as strings with concatenation form a free monoid, i.e. for two strings which have just been generated, concatenation will produce a string that hasn't yet been generated. We need to provide 1-letter strings as atoms, however. Since our algorithm cares more about letters between 'a' and 'e', we will influence the distribution.

So we start to write a string generator, we want to generate a kilo of them. We also need a proven pseudo-random engine.

bool test_getList(std::mt19937& engine) {
  auto string_generator =

Now we include the first operation, the one that gives 1-letter strings. We try to generate more strings with the letter between 'a' and 'e'.

   ([&engine] () {
     char c;
     if (std::uniform_int_distribution<int>(0,2)(engine))
       c = std::uniform_int_distribution<char>('a', 'e')(engine);
       c = std::uniform_int_distribution<char>()(engine);
     return std::string(1u, c);

Now we can add the concatenation operation.

   std::function<std::string(const std::string&,
                             const std::string&)>
   ([] (const std::string& a,
        const std::string& b) { return a + b; }));

string_generator generates strings. However we need streams. We can make another generator and easily reuse string_generator.

There are a few annoying things with generating streams. First, we need to generate std::istream which is abstract, which means not copyable and not move-able. The generator will detect it is not possible to store them, and a workaround is required. We could have an operation returning references to std::istringstream objects, which are supposed to be normally move-able, but unfortunately are not yet in GCC versions up to 4.6.0. So instead we will deal with pointers. std::unique_ptr can be used as it is movable, and it will be just enough to store the streams somewhere in the memory.

We start defining our generator by reusing the previous generator.

  auto generator =

Now we provide a way to construct string streams.

       std::function<std::unique_ptr<std::istringstream>(const std::string&)>
       ([] (const std::string& s) -> std::unique_ptr<std::istringstream>
       { return std::unique_ptr<std::istringstream>(new std::istringstream(s)); }),

Finally we provide a conversion from string streams to abstract streams.

       std::function<std::istream&(std::unique_ptr<std::istringstream>& i)>
       ([] (std::unique_ptr<std::istringstream>& i) -> std::istream&
       { return *i; }));

This generator will unfortunately never generate the empty string. But since our axiom has only one parameter, we can easily just test this special case manually.

  std::istringstream in{std::string{}};
  if (!catch_errors(axiom, in))
    return false;

Now we can run the test.

  if (!test(generator, axiom, "axiom"))
    return false;

  return true;