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:
- Joris Peters https://github.com/jorisptrs
- Rienk Bergsma https://github.com/Dragonflew17
- Tait van Strien https://gitlab.com/7A1T
- Tino Alferink https://gitlab.com/Tinoalfie
- Tudor Roscoiu https://gitlab.com/tudoroscoiu