▼Redex: Debugging Operational Semantics
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
Version: 4.2.1
  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 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 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 error

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

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 →