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

Question

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

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

Answer 1

事实证明，如果您可以将 redex 术语赋予您的实际实现，或者将它们转换为适合您的实现，那么redex-check当与直接结合使用时，可以直接处理它。apply-reduction-relation*您的代码将如下所示：

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

您可以在 redex 主页redex-check上的教程中看到另一个如何使用的示例。