使用PLT-Redex测试语义时仅生成类型良好的术语
使用PLT-Redex测试语义时仅生成类型良好的术语
提问于 2017-08-17 04:42:48
我是个球拍新手，我对使用redex特别感兴趣。我为类型化的算术表达式做了一个小模型，可以在皮尔斯的《类型和编程语言》一书中找到。代码的要点如下：https://gist.github.com/rodrigogribeiro/e0fd3e1e3ff017b614dcfeee9f9154e0
当我尝试测试进度和保存等属性时，我想检查测试覆盖了多少代码，因此我运行了以下代码，如amb教程中所示：
(let ([c (make-coverage red)])
(parameterize ([relation-coverage (list c)])
(check-reduction-relation
red
(λ (E) (progress-holds? E)))
(covered-cases c)))但是，它返回
'(("E-if-false" . 0) ("E-if-true" . 0) ("E-iszero-suc" . 0)
("E-iszero-zero" . 0) ("E-pred-suc" . 0) ("E-pred-zero" . 0))这意味着语义的任何规则都不会执行，对吧？我认为问题在于problem生成的随机术语并不一定是正确键入的。
我的问题是:有没有一种方法可以指定如何只生成类型良好的术语？
回答 1
Stack Overflow用户
回答已采纳
发布于 2017-09-02 07:18:59
经过几次尝试和重新做这个小练习，我得到了一个合理的解决方案(完整的代码在下面的gist中)。只生成类型良好的术语的要点是使用#:satisfying子句约束redex生成器，比如下面的progress属性测试：
(define (progress)
(let ([c (make-coverage eval-tyexp)])
(parameterize ([relation-coverage (list c)])
(redex-check TyExp
#:satisfying (types e t)
(progress-holds? (term e)))
(covered-cases c))))行#:satisfying (types e t)说，只有判断types e t持有的表达式e才应该被考虑。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/45722671
复制相关文章
相似问题
腾讯云开发者
