2017-09-16 22:10:55 +03:00
|
|
|
resolver: nightly-2016-06-20
|
2015-10-08 14:05:59 +03:00
|
|
|
|
2015-07-19 06:39:39 +03:00
|
|
|
packages:
|
2016-06-20 23:45:34 +03:00
|
|
|
- concurrency
|
2015-10-05 18:44:14 +03:00
|
|
|
- dejafu
|
2015-12-01 08:03:31 +03:00
|
|
|
- dejafu-tests
|
2016-06-20 23:45:34 +03:00
|
|
|
- hunit-dejafu
|
|
|
|
|
- tasty-dejafu
|
2015-10-08 14:05:59 +03:00
|
|
|
|
2017-03-20 21:42:51 +03:00
|
|
|
extra-deps:
|
|
|
|
|
- call-stack-0.1.0
|
|
|
|
|
- HUnit-1.6.0.0
|
Implement refinement property testing
This lets dejafu test CoCo-style properties, and introduces a
dependency on [leancheck][].
For example, consider this statement about MVars: "using readMVar is
better than a takeMVar followed by a putMVar because the former is
atomic but the latter is not."
This module can test properties like that:
```
sig e = Sig
{ initialise = maybe newEmptyMVar newMVar
, observe = \v _ -> tryReadMVar v
, interfere = \v s -> tryTakeMVar v >>
maybe (pure ()) (void . tryPutMVar v) s
, expr = e
}
> check $ sig (void . readMVar) `equivalentTo`
sig (\v -> takeMVar v >>= putMVar v)
*** Failure: (seed Just ())
left: [(Nothing,Just ())]
right: [(Nothing,Just ()),(Just Deadlock,Just ())]
```
The two expressions are not equivalent, and we get given the
counterexample!
In addition to "equivalentTo", there is also "refines" and
"strictlyRefines" (and negated variants)
[leancheck]: https://hackage.haskell.org/package/leancheck
2017-05-31 15:15:50 +03:00
|
|
|
- leancheck-0.6.2
|
2017-09-16 22:10:55 +03:00
|
|
|
- test-framework-hunit-0.3.0.2
|
2017-03-20 21:42:51 +03:00
|
|
|
|
|
|
|
|
nix:
|
|
|
|
|
packages: [git]
|
