将模型与 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 的另一个示例。