PBT Tests - Githubissues

informalsystems / quint

An executable specification language with delightful tooling based on the temporal logic of actions (TLA)

Apache License 2.0

804 stars 31 forks source link

PBT Tests #82

Open bugarela opened 2 years ago

bugarela commented 2 years ago

We don't have any setup for property-based testing. Pointed out by @shonfeder at https://github.com/informalsystems/tnt/pull/81/files#r853271142. I can see that helping a lot with testing since writing unit tests for individual IR components is already too much - testing combinations of them is unfeasible without PBT.

shonfeder commented 2 years ago

This might be a useful and easy place for me to begin contributing work. Some first steps would include:

[ ] Identify feasible PBT libraries
[ ] Select a library to use
[ ] Write generators for atomic values
[ ] Write generators for compound values
[ ] Write generators for types
[ ] Come up with a list of places where PBTs could be especially useful

shonfeder commented 8 months ago

We talked at the end of last year about having some PBT over our IR might turn up edge cases, which, currently, are left for users to discover :)