Property Based Tests / Proofs
This milestone gathers all efforts related to Property Based Testing (PBT) and Coq proofs (as there are possible bridges between PBTs and Coq proofs, see below).
This is a part of the overall Test effort of Tezos.
The high level goal of both PBTs and proofs is to increase productivity of developers and lowering costs by improving the software quality of Tezos (or achieving the same quality with fewer efforts).
Property Based Tests
Complementary to Unit tests
PBTs are loosely comparable to unit tests, with some noticeable differences:
- they generate many tests (default: 100 per written PBT) by generating pseudo-random unbiased inputs, which helps exploring corner cases and find bugs more efficiently than unit tests
- they additionally enable testing properties of a function (or set of functions), e.g. "add and subtract cancel each other" to test functions are consistent
Note that the goal is not to remove unit tests, but to have both. Unit tests are better seen as checked examples (helps readers grasp what a function does on specific examples) while PBTs actually express and check "the general case".
PBT work - Done already
-
Migrate to a better PBT library called QCheck -
Migrate existing unit tests to PBTs (a majority of unit tests can be generalized to invariance PBTs) -
Fix of a bug in Time.Protocol
found thanks to PBTs
PBT work - To be done
Coq-of-OCaml
While PBTs express properties that are tested against an arbitrary number of pseudo-random inputs, a passing PBT is an absence of evidence of a bug, not an evidence of absence of bug.
One step further in checking the quality of parts of Tezos is to use a proof assistant like Coq to check some properties are always true (hence those properties are never bugged).
This is the role of the Coq Tezos of OCaml (CTOC) project.
Additionally there are some ideas on how to further integrate PBTs with CTOC.
Other interesting things that can't be linked in this milestone (Gitlab limitations)
- QCheck improvements: see %Property Based Tests: QCheck Improvements