基于树自动机的成功类型
Towards Tree Automata-based Success Types
摘要:
动态语言的错误检测工具通常基于单元测试。因此,快速原型和灵活性的优势必须与繁琐和耗时的测试套件开发相权衡。Lindahl和Sagonas的成功类型提供了一种在Erlang中进行静态must-fail检测的方法。由于该方法基于约束的性质,无法检测到涉及嵌套元组和递归的一些错误。我们提出了一种方法,使用扩展的模型检验的模式匹配递归方案与上下文感知的排名树自动机,以提供改进的成功类型为基础的一阶原型语言。
英文摘要:
Error detection facilities for dynamic languages are often based on unit testing. Thus, the advantage of rapid prototyping and flexibility must be weighed against cumbersome and time consuming test suite development. Lindahl and Sagonas' success typings provide a means of static must-fail detection in Erlang. Due to the constraint-based nature of the approach, some errors involving nested tuples and recursion cannot be detected. We propose an approach that uses an extension of model checking for pattern-matching recursion schemes with context-aware ranked tree automata to provide improved success typings for a constructor-based first-order prototype language.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。