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).

If #:pred is specified, it is applied to each reachable term until one of the terms fails to satify the predicate (i.e., the predicate returns #f). If that happens, then the test fails and a message is printed with the term that failed to satisfy the predicate.

This test uses apply-reduction-relation*, so it does not terminate when the resulting reduction graph is infinite.

Examples:

> (define-language L       (i integer))

> (define R       (reduction-relation        L        (--> i i)        (--> i ,(add1 (term i)))))

> (define (mod2=? i j)       (= (modulo i 2) (modulo j 2)))

> (test--> R #:equiv mod2=? 7 1)

FAILED :9.0   expected: 1     actual: 8     actual: 7

> (test--> R #:equiv mod2=? 7 1 0)

> (test-results)

1 test failed (out of 2 total).

Examples:

> (define-language L       (n natural))

> (define succ-mod8       (reduction-relation        L        (--> n ,(modulo (add1 (term n)) 8))))

> (test-->>∃ succ-mod8 6 2)

> (test-->>∃ succ-mod8 6 even?)

> (test-->>∃ succ-mod8 6 8)

FAILED :16.0   no reachable term equal to 8

> (test-->>∃ #:steps 6 succ-mod8 6 5)

FAILED :17.0   no reachable term equal to 5 (but some terms were not unexplored)

> (test-results)

2 tests failed (out of 4 total).

Examples:

> (define-language empty-lang)

> (define-metafunction empty-lang       [(plus number_1 number_2)        ,(+ (term number_1) (term number_2))])

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

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

'(("add" . 2) ("eval:21:0" . 1) ("zero" . 0))

'(("eval:20:0" . 2))

The argument size-expr bounds the height of the generated term (measured as the height of its parse tree).

The optional keyword argument attempt-num-expr (default 1) provides coarse grained control over the random decisions made during generation; increasing attempt-num-expr tends to increase the complexity of the result. For example, the expected length of pattern-sequences increases with attempt-num-expr.

The random generation process does not actively consider the constraints imposed by side-condition or _!_ patterns; instead, it uses a “guess and check” strategy in which it freely generates candidate terms then tests whether they happen to satisfy the constraints, repeating as necessary. The optional keyword argument retries-expr (default 100) bounds the number of times that generate-term retries the generation of any pattern. If generate-term is unable to produce a satisfying term after retries-expr attempts, it raises an exception recognized by exn:fail:redex:generation-failure?.

redex-check generates at most attempts-expr (default 1000) random terms in its search. The size and complexity of these terms tend to increase with each failed attempt. The #:attempt-size keyword determines the rate at which terms grow by supplying a function that bounds term size based on the number of failed attempts (see generate-term’s #:size keyword). By default, the bound grows according to the default-attempt-size function.

The optional #:prepare keyword supplies a function that transforms each generated example before redex-check checks property-expr. This keyword may be useful when property-expr takes the form of a conditional, and a term chosen freely from the grammar is unlikely to satisfy the conditional’s hypothesis. In some such cases, the prepare keyword can be used to increase the probability that an example satifies the hypothesis.

When passed a metafunction or reduction relation via the optional #:source argument, redex-check distributes its attempts across the left-hand sides of that metafunction/relation by using those patterns, rather than pattern, as the basis of its generation. It is an error if any left-hand side generates a term that does not match 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 ...))))))

redex-check: counterexample found after 5 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: no counterexamples in 200 attempts

> (let ([R (reduction-relation               empty-lang               (--> (Σ) 0)               (--> (Σ number) number)               (--> (Σ number_1 number_2 number_3 ...)                    (Σ ,(+ (term number_1) (term number_2))                       number_3 ...)))])       (redex-check        empty-lang        (Σ number ...)        (printf "~s\n" (term (number ...)))        #:attempts 3        #:source R))

()   (1)   (3 0)   redex-check: no counterexamples in 1 attempt (with each clause)

> (redex-check      empty-lang      number      (begin        (printf "checking ~s\n" (term number))        (positive? (term number)))      #:prepare (λ (n)                  (printf "preparing ~s; " n)                  (add1 (abs n)))      #:attempts 3)

preparing 0; checking 1   preparing 0; checking 1   preparing 1; checking 2   redex-check: no counterexamples in 3 attempts

Examples:

> (define-language empty-lang)

> (random-seed 0)

> (define-metafunction empty-lang       Σ : number ... -> number       [(Σ) 0]       [(Σ number) number]       [(Σ number_1 number_2 number_3 ...)        (Σ ,(+ (term number_1) (term number_2)) number_3 ...)])

> (check-metafunction Σ (λ (args) (printf "~s\n" args)) #:attempts 2)

()   ()   (0)   (0)   (2 1)   (0 1)   check-metafunction: no counterexamples in 2 attempts (with each clause)

Debugging PLT Redex Programs

It is easy to write grammars and reduction rules that are subtly wrong. Typically such mistakes result in examples that 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, then try to find out which pattern is failing to match. To do so, use the redex-match form.

In particular, first check if the term in question matches the your system’s main non-terminal (typically the expression or program non-terminal). If it does not match, simplify the term piece by piece to determine whether the problem is in the term or the grammar.

If the term does match your system’s main non-terminal, determine by inspection which reduction rules should apply. For each such rule, repeat the above term-pattern debugging procedure, this time using the rule’s left-hand side pattern instead of the system’s main non-terminal. In addition to simplifying the term, also consider simplifying the pattern.

If the term matches the left-hand side, but the rule does not apply, then one of the rule’s side-condition or where clauses is not satisfied. Using the bindings reported by redex-match, check each side-condition expression and each where pattern-match to discover which clause is preventing the rule’s application.