▼ |  | Redex: Practical Semantics Engineering

1 | Patterns
2 | Terms
3 | Languages
4 | Reduction Relations
5 | Metafunctions and Relations
6 | Testing
7 | GUI
8 | Typesetting
| Index

On this page:

test-equal
test-->>
test-->
test-predicate
test-results
make-coverage
coverage?
relation-coverage
covered-cases
generate-term
redex-check
check-reduction-relation
check-metafunction
exn: fail: redex: generation-failure?

top← prev up next →

### 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 maybe-cycles e1 e2 ...)

cycles

=

|  | | |  | #:cycles-ok

Tests to see if the value of e1 (which should be a term), reduces to the e2s under reduction-relation (using apply-reduction-relation*, so it may not terminate).

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

Tests to see if the value of e1 (which should be a term), reduces to the e2s in a single step, under reduction-relation (using apply-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 subject)

subject |  | = |  | metafunction
|  | | |  | relation-expr

Constructs a structure (recognized by coverage?) to contain per-case test coverage of the supplied metafunction or reduction relation. 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) → (listof coverage?)
(relation-coverage tracked) → void?
tracked : (listof coverage?)

Redex populates the coverage records in tracked (default null), counting the times that tests exercise each case of the associated metafunction and relations.

(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 (or source locations, in the case of metafunctions or unnamed reduction-relation cases) to application counts.

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

(("eval:4:0" . 1) ("zero" . 0) ("add" . 2))
(("eval:3:0" . 2))

(generate-term language pattern size-exp kw-args ...)

kw-args |  | = |  | #:attempts attempts-expr
|  | | |  | #:retries retries-expr

> | size-expr |  | : |  | natural-number/c

> | attempt-num-expr |  | : |  | natural-number/c

> | retries-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. 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 when constructing a term; instead, it tests the satisfaction of such constraints after it freely generates the relevant portion of the sub-term – regenerating the sub-term if necessary. The optional keyword argument retries-expr (default 100) bounds the number of times that generate-term retries the generation of any sub-term. 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 language pattern property-expr kw-arg ...)

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

> | property-expr |  | : |  | any/c

> | attempts-expr |  | : |  | natural-number/c

> | relation-expr |  | : |  | reduction-relation?

> | retries-expr |  | : |  | natural-number/c

Searches for a counterexample to property-expr, interpreted as a predicate universally quantified over the pattern variables bound by pattern. redex-check constructs and tests a candidate counterexample by choosing a random term t that matches pattern then evaluating property-expr using the match-bindings produced by matching t against pattern.

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

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

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

(check-reduction-relation relation property kw-args ...)

kw-arg |  | = |  | #:attempts attempts-expr
|  | | |  | #:retries retries-expr

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

> | attempts-expr |  | : |  | natural-number/c

> | retries-expr |  | : |  | natural-number/c

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

This form provides a more convenient notation for

(redex-check L any (property (term any))
#:attempts (* n attempts)
#:source relation)

when relation is a relation on L with n rules.

(check-metafunction metafunction property kw-args ...)

kw-arg |  | = |  | #:attempts attempts-expr
|  | | |  | #:retries retries-expr

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

> | attempts-expr |  | : |  | natural-number/c

> | retries-expr |  | : |  | natural-number/c

Like check-reduction-relation but for metafunctions.

(exn:fail:redex:generation-failure? v) → boolean?
v : any/c

Recognizes the exceptions raised by generate-term, redex-check, etc. when those forms are unable to produce a term matching some pattern.

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

top← prev up next →