|
|
|
|
|
by mcguire
2708 days ago
|
|
Normal testing feeds selected inputs to the software and succeeds for the corresponding output. QuickCheck feeds random values to the software and looks for "good" results. TLA+ takes a model of the system (not the software) and explores the entire state space and looks for anything that violates given logical predicates. It is a different later of abstraction. |
|