Information Technology Reference
In-Depth Information
(2) how expensive is it to check that equations follow from other equations, (3)
not removing too many equations (even though an equation follows from other
ones, it might still be useful to have in the list). The algorithm we finally settled
for uses a congruence closure algorithm to approximate if an equation follows
from a set of equations.
We have applied QuickSpec to a number of concrete Erlang and Haskell mod-
ules. Most notably, we applied it on the Erlang standard functional array library,
and on a library for fixed-point arithmetic that was written by a company in
South Africa. Exploring the properties that QuickSpec produced (and the prop-
erties it did not produce!) was a great way of understanding code that someone
else had written, and has lead us to come up with a number of concrete tech-
niques that may be used for applying QuickSpec in this way. Other applications
of QuickSpec include providing a cheap and easy way for programmers and
testers to start writing properties.
3.2
Reverse Engineering
We have developed two methods to extract properties from test cases - one
dynamic, the other static. That is, in the first approach, the test cases are run,
generating traces for the program. From these traces a finite state machine can
be abstracted. This is described fully in the companion paper [WD09] as well as
in [WDG09].
The second approach works on the level of the source code of the test cases. It
is a guided automatic approach; testers know best what part of the test case they
like to generate and what part they want to keep specific. Recent work with test
suites from Ericsson, and with tests from an Open Source project (Engineyard's
Natter application) confirm that this approach is a fruitful one.
3.3
Building Domain Specific Languages
QuickCheck has long provided a DSL (Domain Specific Language) for specifica-
tions based on abstract state machines; however, this DSL represents states as
arbitrary Erlang data values - for example, a list of key-value pairs if modeling
a key-value store. With this approach, each operation of the API under test is
applicable in every state, unless an explicit precondition is given to restrict this.
Software is commonly specified instead via a state transition diagram, in which
states are distinguished by name, and operations are typically applicable only
in a certain named state.
Of course, such a specification can be based on the previous state machine
library, but doing so in effect encodes the structure of the diagram in an ugly
way in many different places in the code.
To help overcome this, we have developed a new FSM library, implemented on
top of the original one, which separates state names and state data. Specifications
using the new library are much more concise and perspicuous than the equivalent
specification using the old one. Our FSM library allows weights to be assigned
to transitions, but assigning weights well is dicult, since changing a weight
