Generating Well-Typed Terms That Are Not “Useless”
Generating Well-Typed Terms That Are Not “Useless”
复制标题
生成类型正确但并非“无用”的术语
DOI：
10.1145/3632919
复制
发表时间：
2024
影响因子：
--
通讯作者：
Lampropoulos, Leonidas
中科院分区：
文献类型：
--
作者：
Frank, Justin;Quiring, Benjamin;Lampropoulos, Leonidas
好类型术语的随机生成是函数式语言编译器有效随机测试的核心。现有的技术已经成功地遵循了一种自上而下的面向类型的方法来生成，这种方法在本地做出选择，这受到固有的限制：表达式的类型通常是独立于表达式本身生成的。这样的生成通常会生成参数类型不能用于以有意义的方式生成结果的函数，从而不使用这些参数。由于参数生成代码已死，但仍需编译，这类“不用”的函数可能会同时影响性能和效率，因为许多有趣的优化不太频繁地被测试。在本文中，我们介绍了一种新的算法，该算法在生成使用其参数的函数时明显更有效。在带有类型和参数漏洞的简单类型Lambda演算的扩展中，我们将“局部”和“非局部”算法都形式化为步骤关系，展示了如何通过允许非局部生成步骤来延迟子表达式的类型生成，从而产生“有用的”函数。
Random generation of well-typed terms lies at the core of effective random testing of compilers for functional languages. Existing techniques have had success following a top-down type-oriented approach to generation that makes choices locally, which suffers from an inherent limitation: the type of an expression is often generated independently from the expression itself. Such generation frequently yields functions with argument types that cannot be used to produce a result in a meaningful way, leaving those arguments unused. Such "use-less" functions can hinder both performance, as the argument generation code is dead but still needs to be compiled, and effectiveness, as a lot of interesting optimizations are tested less frequently.In this paper, we introduce a novel algorithm that is significantly more effective at generating functions that use their arguments. We formalize both the "local" and the "nonlocal" algorithms as step-relations in an extension of the simply-typed lambda calculus with type and arguments holes, showing how delaying the generation of types for subexpressions by allowing nonlocal generation steps leads to "useful" functions.
登录
查看更多内容
做出随机判断：根据类型系统的定义自动生成类型良好的术语
DOI：
--
发表时间：
2015
期刊：
European Symposium on Programming
影响因子：
--
作者：
B. Fetscher;Koen Claessen;Michal H. Palka;John Hughes;R. Findler
通讯作者：
R. Findler
检查C的形式化模型
DOI：
10.1109/csf54842.2022.9919657
发表时间：
2022
期刊：
2022 IEEE 35th Computer Security Foundations Symposium (CSF
影响因子：
--
作者：
Li, Liyi;Liu, Yiyun;Postol, Deena;Lampropoulos, Leonidas;Van Horn, David;Hicks, Michael
通讯作者：
Hicks, Michael
使用 QuickCheck 生成随机类型良好的轻量级 Java 程序
DOI：
10.1016/j.entcs.2019.04.002
发表时间：
2019
期刊：
Drug metabolism and disposition: the biological fate of chemicals
影响因子：
--
作者：
Samuel da Silva Feitosa;R. Ribeiro;A. R. D. Bois
通讯作者：
A. R. D. Bois
用于封闭式简单类型 Lambda 项的玻尔兹曼采样器
DOI：
10.1007/978-3-319-51676-9_8
发表时间：
2017
期刊：
Drug metabolism and disposition: the biological fate of chemicals
影响因子：
--
作者：
Maciej Bendkowski;Katarzyna Grygiel;Paul Tarau
通讯作者：
Paul Tarau
活跃度驱动的随机程序生成
DOI：
--
发表时间：
2017
期刊：
International Workshop/Symposium on Logic-based Program Synthesis and Transformation
影响因子：
--
作者：
Gergö Barany
通讯作者：
Gergö Barany