junit-quickcheck State-machine-based testing

Many flavours of QuickCheck (eg: http://www.quviq.com/products/erlang-quickcheck/, http://proper.softlab.ntua.gr/Tutorials/PropEr_testing_of_finite_state_machines.html, http://www.cs.waikato.ac.nz/~marku/mbt/modeljunit/) offer the possibility of specifying properties in terms of finite state machines. This is very convenient when the property being tested has elements of control-flow, e.g.: every time a newly registered user performs a call to "withdraw" before a call to "deposit" is marked as suspicious. The idea is to have pre and post conditions on each machine transition such that the test is a traversal of the state machine which satisfies the preconditions, checking the satisfaction of the postconditions as the test progresses.

Feb 14 '16 04:02 ccol002

@ccol002 Sorry it's taken me so long to respond here. Do you have a particular API in mind for this feature? What might the junit-quickcheck way of specifying and verifying the FSM look like?

Aug 31 '16 20:08 pholser

@pholser Thanks for getting back. Perhaps the best description of what I have in mind is given here: http://proper.softlab.ntua.gr/Tutorials/PropEr_testing_of_finite_state_machines.html

Please let me know if you need further clarification.

Sep 01 '16 12:09 ccol002

@ccol002 I'm wondering whether mimicking ScalaCheck's support for stateful testing might be a good start? http://scalacheck.org/files/scaladays2014/#1

Sep 28 '16 20:09 pholser

@pholser Yes, that would be very useful as it is easy to model a state machine with that setup.

Sep 29 '16 08:09 ccol002