erlang and quickcheck

erlang and quickcheck

Post by Ulf Wige » Wed, 11 Oct 2006 23:36:11



Some of you may have noticed a presentation given at the
ICFP06 Erlang Workshop in Portland:

"Testing Telecoms Software with Quviq QuickCheck"
(Arts, Hughes, Johansson, Wiger)

I couldn't find the paper in the ACM library yet, but
I'm sure it will turn up eventually.

Many of you surely know QuickCheck from Haskell.
I thought I'd bring attention to a discussion (pg 8)
where Erlang and Haskell are compared as languages for
writing the kind of properties used in QuickCheck.
I found the passage interesting, not least because it was
written by Prof. John Hughes, co-inventor of Haskell and
Erlang Programmer Extraordinaire.

(I've wikified the text slightly).

"Static typing would certainly have been useful to catch errors
in generators earlier, although we found QuickCheck testing to be
quite a good substitute. The original QuickCheck also allows a
default generator to be associated with each type, so that properties
can be formulated a little more simply when the default generator
is appropriate. However, in this case study, /type/ information is not
enough to determine which generator is appropriate - we need to
know the abstract proxy state too. So in this case, the advantage
of using type information to guide generation would be small.

"On the other hand, representing test cases symbolically in Haskell
requires type definitions, potentially many such, whereas in Erlang
we could simply write down the values we wanted. Moreover, the
kind of processing that `eqc_commands' does of test cases would
require sophisticated generic programming in Haskell, but was
much simpler in Erlang. Interpreting symbolic test cases was eased
by Erlang's ability to invoke a function given its /name/ as an Erlang
atom - Erlang provides some basic reflection via this mechanism.

"We conclude that Erlang is rather a suitable host language for this
kind of testing. It's dubious whether our specifications could have
been expressed as concisely in Haskell, even if the versions of
QuickCheck were otherwise equivalent."


One may make several observations. Here are two of mine:

- For those of you out there doing bread and butter programming,
but play with Haskell and QuickCheck on your spare time, it
may be inspiring to see an industrial case study using QuickCheck
for black-box testing. You can approach your bosses with great
confidence. ;-)
- The pilot project was a success, as were the subsequent courses
for some of our designers. This looks to become yet a very nice
industrial application of techniques risen from the Haskell ranks.
QuickCheck certainly is an amazing tool.


BR,
Ulf W
--
Ulf Wiger, Senior Specialist,
/ / / Architecture & Design of Carrier-Class Software
/ / / Team Leader, Software Characteristics
/ / / Ericsson AB, IMS Gateways
 
 
 

erlang and quickcheck

Post by Vesa Karvo » Thu, 12 Oct 2006 15:41:24

lf Wiger < XXXX@XXXXX.COM > wrote:
[...]

If by the "write down the values we wanted" part you mean that one
writes down a type-index (e.g. "list(int ())" from the paper, which I
haven't yet read) rather than a type, then I'm pretty sure that you
could implement a similar interface in Haskell. In fact, you can even
implement it in Standard ML. Below is an example test definition
using a testing framework that I've been developing in SML.

--Vesa Karvonen

(*
* Simple examples of specifying QuickCheck -style randomized tests using
* the UnitTest framework. The example laws are from the QuickCheck paper
* by Koen Claessen and John Hughes.
*)

local
open Type UnitTest

local
fun mk f = f #n Int.compare

(* The functions in the SortedList module are parameterized on both
* a duplicate cardinality (either #1 or #n duplicates are allowed
* and produced) and an ordering (a compare function).
*)

open SortedList
in
val insert = mk insert
val isSorted = mk isSorted
val stableSort = mk stableSort
end

val sortedList =
let
val l = list int
in
withGen (RanQD1Gen.prj (arbitrary l) stableSort) l
end

(* Note that one can (of course) make local auxiliary definitions, like
* here, to help with testing.
*)
in
val () =
unitTests
(title "Reverse")

(chk (all int
(fn x =>
that (rev [x] = [x]))))

(* Read the above as:
*
* "check for all integers x that the reverse of the singleton
* list x equals the singleton list x"
*
* (Of course, in reality, the property is only checked for a
* small finite number of random integers at a time.)
*
* In contrast to QuickCheck/Haskell, one must explicitly lift
* boolean values to properties using {that}.
*)

(chk (all (sq (list int))
(fn (xs, ys) =>
that (rev (xs @ ys) = rev ys @ rev xs))))

(chk (all (list int)
(fn xs =>
that (rev (rev xs) = xs))))

(title "Functions")

let
infix ===
fun (f === g) x = that (f x = g x)
(* An approximation of extensional equality for functions. *)
in
chk (all (uop int &` uop int &` uop int)
(fn f & g & h =>
all int
(f o (g o h) === (f o g) o h)))

(* Note that one can (of course) also write local auxiliary
* definitions inside let -expressions.
*)
end

(title "Conditional laws")

(chk (all (sq int)
(fn (x, y) =>
if x <= y then
that (Int.max (x, y) = y)
else
skip)))

(* Read the above as:
*
* "check for all integer pairs (x, y) that
* if x <= y then max (x, y) = y"
*
* In contrast to QuickCheck/Haskell, conditional properties are
* specified using conditionals and {skip} rather than using an

 
 
 

erlang and quickcheck

Post by Ulf Wige » Thu, 12 Oct 2006 18:07:54

>>>>> "V" == Vesa Karvonen < XXXX@XXXXX.COM > writes:


>> "On the other hand, representing test cases symbolically in
>> Haskell requires type definitions, potentially many such,
>> whereas in Erlang we could simply write down the values we
>> wanted. [...]"

V> If by the "write down the values we wanted" part you mean that
V> one writes down a type-index (e.g. "list(int ())" from the paper,
V> which I haven't yet read) rather than a type, then I'm pretty
V> sure that you could implement a similar interface in Haskell. In
V> fact, you can even implement it in Standard ML. Below is an
V> example test definition using a testing framework that I've been
V> developing in SML.

Well, John does note in his paper that the Haskell version is
slightly more convenient when the standard generators are
sufficient, but that was not the case here. Some of the
generators became quite contrived in order to properly reflect
oddities in the related ITU specification and further restrictions
imposed by our Interwork Specification. I can only refer
to the paper and recommend reading it as it becomes available.

Especially the state machine properties rely on an intricate
combination of symbolic values (used when generating sequences)
and concrete values (known only at run-time), where some
constraints operate on both symbolic and real data.

With a dynamically typed, pattern matching declarative language,
the main challenge becomes to keep these distinctions straight in
your head, but then, writing the actual Erlang code is not
especially difficult.

The other thing to note is that even if confusion about the
types causes problems, QuickCheck will be quick to find an
error in your specification. The way John put it: "Static
typing would certainly have been useful to catch errors in
generators earlier, although we found QuickCheck testing to
be quite a good substitute."

It would surely be an interesting challenge for some to adapt
John's framework(*) to Haskell and/or ML, even though from a
commercial perspective, adapting it to C# or Python would
probably be of greater interest. ;-)

The good news for those of us goofing around in dynamically
typed languages, such as erlang, tools like Dialyzer and
QuickCheck do offer quite a few of the comforts normally
associated with static typing. (:

(*) You'd have to do this in cooperation with John, as it's
a commercial product.

BR,
Ulf W
--
Ulf Wiger, Senior Specialist,
/ / / Architecture & Design of Carrier-Class Software
/ / / Team Leader, Software Characteristics
/ / / Ericsson AB, IMS Gateways
 
 
 

erlang and quickcheck

Post by Vesa Karvo » Thu, 12 Oct 2006 19:25:59


[...]

If you mean

http://www.yqcomputer.com/ %20ERLANG%20Workshop&CFID=15151515&CFTOKEN=6184618

(lovely URL...) then it seems to be available already.

--Vesa Karvonen
 
 
 

erlang and quickcheck

Post by Ulf Wige » Thu, 12 Oct 2006 20:14:59

>>>>> "V" == Vesa Karvonen < XXXX@XXXXX.COM > writes:


>> I can only refer to the paper and recommend reading it as it
>> becomes available. [...]

V> If you mean

V> http://www.yqcomputer.com/ %20ERLANG%20Workshop&CFID=15151515&CFTOKEN=6184618

V> (lovely URL...) then it seems to be available already.

Yes, that's the one. Thanks.

/Ulf W
--
Ulf Wiger, Senior Specialist,
/ / / Architecture & Design of Carrier-Class Software
/ / / Team Leader, Software Characteristics
/ / / Ericsson AB, IMS Gateways