Property based testing with Newton

[KomaGR]

Contemplate the utility of Newton (invariants) as specifications for property based testing. I got this idea from this paper.

[KomaGR]

One thought would be for Newton invariants to provide constraints for the inputs of C functions. A backend would read these invariants and automatically generate testcases for the functions or even perform them itself (unit testing). This would be similar to quickcheck.

For example consider the following function in C:

int 
add(int n1, int n2)
{
  return n1+n1;
}

I want to test this implementation of add. I write the following invariant that specifies the properties I want from my function:

props_add : invariant (n1 : Integer, n2 : Integer, n3 : Integer)
{
  n1 ~ add(n1, n2)                                # Closure
  add(n1, n2) == add(n2, n1),                     # Commutativity
  add(n1, 0) == n1,                               # Identity (right)
  add(0, n2) == n2,                               # Identity (left)
  add(add(n1, n2), n3) == add(n1, add(n2, n3))    # Associativity
}