6 Testing

All of the exports in this section are provided both by redex/reduction-semantics (which includes all non-GUI portions of Redex) and also exported by redex (which includes all of Redex).

(test-equal e1 e2)

Tests to see if e1 is equal to e2.

(test--> reduction-relation e1 e2 ...)

Tests to see if the value of e1 (which should be a term), reduces to the e2s under reduction-relation.

(test-predicate p? e)

Tests to see if the value of e matches the predicate p?.

(test-results) → void?

Prints out how many tests passed and failed, and resets the counters so that next time this function is called, it prints the test results for the next round of tests.

(make-coverage r) → coverage?

r : reduction-relation?

Constructs a structure to contain the per-case test coverage of the relation r. Use with relation-coverage and covered-cases.

(coverage? v) → boolean?

v : any/c

Returns #t for a value produced by make-coverage and #f for any other.

(relation-coverage) → (or/c false/c coverage?)

(relation-coverage c) → void?

c : (or/c false/c coverage?)

When c is a coverage structure, rather than #f (the default), procedures such as apply-reduction-relation, traces, etc. count the number applications of each case of the reduction-relation, storing the results in c.

(covered-cases c) → (listof (cons/c string? natural-number/c))

c : coverage?

Extracts the coverage information recorded in c, producing an association list mapping names to application counts.

Examples:

> (define-language empty-lang)

> (define equals       (reduction-relation        empty-lang        (--> (+) 0 "zero")        (--> (+ number) number)        (--> (+ number_1 number_2 number ...)             (+ ,(+ (term number_1) (term number_2))                number ...)             "add")))

> (let ([coverage (make-coverage equals)])       (parameterize ([relation-coverage coverage])         (apply-reduction-relation* equals (term (+ 1 2 3)))         (covered-cases coverage)))

(("add" . 2) ("unnamed" . 1) ("zero" . 0))

(generate-term language pattern size-exp)

(generate-term language pattern size-exp #:attempt attempt-num-expr)

size-expr   :   natural-number/c    attempt-num-expr   :   natural-number/c

Generates a random term matching pattern (in the given language).

The argument size-expr bounds the height of the generated term (measured as the height of the derivation tree used to produce the term).

The optional keyword argument attempt-num-expr (default 1) provides coarse grained control over the random decisions made during generation (e.g., the expected length of pattern-sequences increases with attempt-num-expr).

(redex-check language pattern property-expr kw-arg ...)

kw-arg   =   #:attempts attempts-expr     |   #:source metafunction     |   #:source relation-expr

property-expr   :   any/c    attempts-expr   :   natural-number/c    relation-expr   :   reduction-relation?

Searches for a counterexample to property-expr, interpreted as a predicate universally quantified over its free term-variables. redex-check chooses substitutions for these free term-variables by generating random terms matching pattern and extracting the sub-terms bound by the names and non-terminals in pattern.

Examples:

> (define-language empty-lang)

> (random-seed 0)

> (redex-check      empty-lang      ((number_1 ...)       (number_2 ...))      (equal? (reverse (append (term (number_1 ...))                               (term (number_2 ...))))              (append (reverse (term (number_1 ...)))                      (reverse (term (number_2 ...))))))

counterexample found after 2 attempts:   ((1 0) (0))

> (redex-check      empty-lang      ((number_1 ...)       (number_2 ...))      (equal? (reverse (append (term (number_1 ...))                               (term (number_2 ...))))              (append (reverse (term (number_2 ...)))                      (reverse (term (number_1 ...)))))      #:attempts 200)

redex-check generates at most attempts-expr (default 100) random terms in its search. The size and complexity of terms it generates gradually increases with each failed attempt.

When the optional #:source argument is present, redex-check generates 10% of its terms by randomly choosing a pattern from the left-hand sides the definition of the supplied metafunction or relation. redex-check raises an exception if a term generated from an alternate pattern does not match the pattern.

(check-reduction-relation   relation             property            [ #:attempts attempts])   →   void?

relation : reduction-relation?

property : (-> any/c any/c)

attempts : natural-number/c = 100

Tests a relation as follows: for each case of relation, check-reduction-relation generates attempts random terms that match that case’s left-hand side and applies property to each random term.

(check-metafunction metafunction property)

(check-metafunction metafunction property #:attempts attempts)

property   :   (-> any/c any/c)    attempts   :   natural-number/c

Like check-reduction-relation but for metafunctions.

Debugging PLT Redex Programs

It is easy to write grammars and reduction rules that are subtly wrong and typically such mistakes result in examples that just get stuck when viewed in a `traces’ window.

The best way to debug such programs is to find an expression that looks like it should reduce but doesn’t and try to find out what pattern is failing to match. To do so, use the redex-match special form, described above.

In particular, first ceck to see if the term matches the main non-terminal for your system (typically the expression or program nonterminal). If it does not, try to narrow down the expression to find which part of the term is failing to match and this will hopefully help you find the problem. If it does match, figure out which reduction rule should have matched, presumably by inspecting the term. Once you have that, extract a pattern from the left-hand side of the reduction rule and do the same procedure until you find a small example that shoudl work but doesn’t (but this time you might also try simplifying the pattern as well as simplifying the expression).