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-->> rel-expr option ... e1-expr e2-expr ...)

option		=		#:cycles-ok
		\|		#:equiv pred-expr

   rel-expr : reduction-relation?
   pred-expr : (--> any/c any/c any/c)
   e1-expr : any/c
   e2-expr : any/c

Tests to see if the term e1-expr, reduces to the terms e2-expr under rel-expr, using pred-expr to determine equivalence. This test uses apply-reduction-relation*, so it does not terminate when the resulting reduction graph is infinite.

(test--> rel-expr option ... e1-expr e2-expr ...)

option

#:equiv pred-expr

   rel-expr : reduction-relation?
   pred-expr : (--> any/c any/c anyc)
   e1-expr : any/c
   e2-expr : any/c

Tests to see if the term e1-expr, reduces to the terms e2-expr in a single rel-expr step, using pred-expr to determine equivalence.

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 :5.0
  expected: 1
    actual: 8
    actual: 7
  > (test--> R #:equiv mod2=? 7 1 0)
  > (test-results)
  1 test failed (out of 2 total).

(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))))
  '(("add" . 2) ("eval:10:0" . 1) ("zero" . 0))
  '(("eval:9:0" . 2))

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

(generate-term language pattern)

kw-args		=		#:attempt-num attempts-expr
		\|		#:retries retries-expr

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

In its first form, generate-term produces a random term matching the given pattern (according to the given language). In its second, generate-term produces a procedure for constructing the same. This procedure expects size-expr (below) as its sole positional argument and allows the same optional keyword arguments as the first form. The second form may be more efficient when generating many terms.

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 language pattern property-expr kw-arg ...)

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

   property-expr : any/c
   attempts-expr : natural-number/c
   relation-expr : reduction-relation?
   retries-expr : natural-number/c
   print?-expr : any/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 these terms increase with each failed attempt.

When print?-expr produces any non-#f value (the default), redex-check prints the test outcome on current-output-port. When print?-expr produces #f, redex-check prints nothing, instead

returning a counterexample structure when the test reveals a counterexample,
returning #t when all tests pass, or
raising a exn:fail:redex:test when checking the property raises an exception.

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))
  ()
  (0)
  (1 0)
  redex-check: no counterexamples in 1 attempt (with each clause)

(struct		counterexample (term)
		#:extra-constructor-name make-counterexample
		#:transparent)

term : any/c

Produced by redex-check, check-reduction-relation, and check-metafunction when testing falsifies a property.

(struct		exn:fail:redex:test exn:fail:redex (source term)
		#:extra-constructor-name make-exn:fail:redex:test)

source : exn:fail?

term : any/c

Raised by redex-check, check-reduction-relation, and check-metafunction when testing a property raises an exception. The exn:fail:redex:test-source component contains the exception raised by the property, and the exn:fail:redex:test-term component contains the term that induced the exception.

(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 : (-> (listof any/c) any/c)
   attempts-expr : natural-number/c
   retries-expr : natural-number/c

Like check-reduction-relation but for metafunctions. check-metafunction calls property with lists containing arguments to the metafunction.

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)

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

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