racket - 比较模型与 Redex 中的实现

Question

我正致力于在类型系统的 Redex 中构建一个模型，该模型也具有规范的实现。我想使用 redex-check 来针对实际实现对我的模型进行模糊测试。

实现(带有适配器)可以采用我的抽象语法，所以我需要的是一种将模糊器生成的术语传递给实现的方法。有办法做到这一点吗？

Answer 1

事实证明redex-check , 当与 apply-reduction-relation* 组合时如果您可以为您的实际实现提供 redex 术语，或者将它们转换为适合您的实现，则直接处理此问题。您的代码将如下所示:

(redex-check λv e
             (equal? (implementation (convert (term e)))
                     (first (apply-reduction-relation* red (term e)))))

implementation 是您的实现，red 是您的模型使用的归约关系，convert 将术语转换为您的实现可以处理的内容.此外，λv 是您的语言，e 是您希望它测试的语言中的术语。

first 只是因为 apply-reduction-relation* 返回所有可能的归约列表。如果您的模型是确定性的，那么这应该是一个长度为 1 的列表。 (您可以使用以下归约关系来检查:

(redex-check λv e
             (let ([result (apply-reduction-relation* red (term e))])
               (and (= (length result) 1)
                    (equal? (implementation (convert (term e)))
                            (first result)))))

您可以在教程 on the redex home page 中看到另一个如何使用 redex-check 的示例.