成功类型的证伪观
A Falsification View of Success Typing
摘要：
动态语言因其灵活性和表达能力而受到称赞，但静态分析经常产生许多误报，并且由于缺乏结构，验证很麻烦。因此，单元测试是验证这些语言程序的流行的不完全方法。证伪是一种可供选择的方法，可以发现程序中的明确错误。证伪者计算一组输入，这些输入肯定会使程序崩溃。成功类型化（Success typing）是一种基于类型的方法，用于在动态语言中记录程序。我们证明，成功的类型，事实上，一个实例的伪造成功（输入）类型映射到合适的逻辑公式。输出类型由递归类型表示。我们证明了我们的映射的正确性（建立成功打字是伪造的），我们报告了一些经验的原型实现。
英文摘要：
Dynamic languages are praised for their flexibility and expressiveness, but static analysis often yields many false positives and verification is cumbersome for lack of structure. Hence, unit testing is the prevalent incomplete method for validating programs in such languages. Falsification is an alternative approach that uncovers definite errors in programs. A falsifier computes a set of inputs that definitely crash a program. Success typing is a type-based approach to document programs in dynamic languages. We demonstrate that success typing is, in fact, an instance of falsification by mapping success (input) types into suitable logic formulae. Output types are represented by recursive types. We prove the correctness of our mapping (which establishes that success typing is falsification) and we report some experiences with a prototype implementation.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
