Property based tests are a way to find bugs in the code by running a boolean function (representing an expected property) on randomly generated inputs. In this blog post, we show how we translate these tests to corresponding Coq theorems. Once we have a formal representation, we prove them correct on any inputs. Thanks to this technique, we can:
- have a bridge between the specification given by the tests and the specification in Coq;
- make sure that the properties verified in the tests are true with a mathematical degree of certainty.
We have done this work with students from the University of Groningen: