The Haystack

The shape of the haystack is defined by a set of "generator bindings," in which variables are bound to the output of value generators:

  x <- Int, c <- Char( charset=>"A-Z" )

The above can be read, "For all integers x and all characters c in the range A through Z." The idea is that each unique instance of the pair (x, c) specifies a point in the haystack that we can search for needles.

The Needle Recognizer

The "needle recognizer" is defined by a snippet of code that uses the bound variables to inspect a given point in the haystack. It returns a "thumbs up" (true) if the point is free of needles or a "thumbs down" (false) if it finds a needle:

  the_thing_we_are_testing($x, $c) >= 0;

The above asserts for each point in the haystack that the output of the function "the_thing_we_are_testing" must be non-negative.

Put them together to make a Property

The generator bindings and needle recognizer are combined to make a property:

  Property {
    ##[ x <- Int, c <- Char( charset=>"A-Z" ) ]##
    the_thing_we_are_testing($x, $c) >= 0;
  }, name => "the_thing_we_are_testing(...) is non-negative";

You'll note that we also added a meaningful name. Although not strictly required, it's an excellent practice that makes life easier. (You'll also note that we placed the generator bindings inside of the magic delimiters "##[ ]##". This tells Perl that our bindings are bindings and not regular Perl code.)

We can read the above property like so: "For all integers x and all characters c in the range A through Z, we assert that "the_thing_we_are_testing" is non-negative."

Testing whether your Properties hold

After you define properties for your software, just add them to a small Perl program that uses the Test::LectroTest module:

  # MyProperties.l.t
  use MyModule;  # provides the_thing_we_are_testing
  use Test::LectroTest;
  Property {
    ##[ x <- Int, c <- Char( charset=>"A-Z" ) ]##
    the_thing_we_are_testing($x, $c) >= 0;
  }, name => "the_thing_we_are_testing(...) is non-negative";

Then you can test your properties simply by running the program:

  $ perl MyProperties.l.t

If your properties check out, you'll see something like this:

  1..1
  ok 1 - 'the_thing_we_are_testing(...) is non-negative' (1000 attempts)

If something goes wrong, however, LectroTest will tell you where it happened:

  1..1
  not ok 1 - 'the_thing_we_are_testing(...) is non-negative' \
    falsified in 23 attempts
  # Counterexample:
  # $x = 4
  # $c = "R"

What this says is that at the point (x=4, c="R") in the haystack, there is a needle (i.e., your property doesn't hold). With this information, you can examine your code to determine the cause of the error.