从复杂规范中合成变换器
摘要：自动化字符串转换一直是程序综合的杀手应用之一。现有解决这个问题的综合器生成领域特定语言（DSL）的程序，这些DSL被设计用来帮助综合器，因此缺乏良好的形式属性。这一限制阻碍了生成的程序在验证应用中的使用（例如检查复杂的前后条件），并使得综合器难以修改，因为它们依赖于给定的DSL。我们提出了一种基于约束的合成转换器的方法，这是一种经过深入研究具有强闭包和可判定性属性的模型。我们的方法处理三种类型的规范：(i) 输入-输出示例，(ii) 表示为正则语言的输入-输出类型，以及(iii) 限制转换器在处理输入字符串时可以修改多少个字符的输入/输出距离。我们的工作是第一个支持这种复杂规范的，并且通过使用转换器的算法属性生成可以使用现成的SMT求解器解决的约束来实现这一目标。我们的综合方法可以扩展到许多转换器模型，并且由于转换器的闭包属性，它可以用于计算部分正确的转换器的修复。
作者：Anvay Grover, Ruediger Ehlers, Loris D'Antoni
论文ID：2208.05131
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2022-08-30