-
Notifications
You must be signed in to change notification settings - Fork 18
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add property-based tests #142
Comments
Goes some way to solving #142, but it would be nice to have some for the memory stuff.
Goes some way to solving #142, but it would be nice to have some for the memory stuff.
Added some tests, but it would be nice to have some for the memory implementation as well. However, I'm not really sure how to best add those, as leancheck doesn't do monadic properties. At the moment |
Goes some way to solving #142, but it would be nice to have some for the memory stuff.
Goes some way to solving #142, but it would be nice to have some for the memory stuff.
Goes some way to solving #142, but it would be nice to have some for the memory stuff.
An alternative to fitting This is probably a far smaller change. |
There are certainly some things which could benefit from property testing, if someone was willing to write the
Arbitrary
orListable
instances. Here are a few I spotted skimming through Test.DejaFu.SCT.Internal:\ds tid act -> canInterrupt ds tid act ==> canInterruptL ds tid (rewind act)
dependentActions
is commutative\mem ds tid1 ta1 tid2 ta2 -> dependent mem ds tid1 ta1 tid2 ta2 ==> dependent' mem ds tid1 ta1 tid2 (rewind ta2)
(I think that should be the case...)I suspect the various Test.DejaFu.Conc.Internal modules and Test.DejaFu.Common will be fruitful as well. Depending on how crazy you want to get, you could even check that
Eq
andOrd
instances are consistent, where one or both is hand-written.This is worthwhile because there's a lot of logic which differs only in whether it accepts a
ThreadAction
or aLookahead
value. TheThreadAction
case is supposed to be the more accurate case, whereas theLookahead
case is supposed to be the more pessimistic case, so checking that (eg with implication if it's a predicate) would help make sure there aren't any mistakes.The text was updated successfully, but these errors were encountered: