代数库规范下的程序合成( 五 ) 1引用BenjaminMariano,JoshReese,Siyu

然而，代数规格存在一些局限性。一些库不适合代数规范，例如，似乎很难以代数形式指定平方根的行为。但是，由于 JLibSketch 还允许进行模拟（它们只是 Sketch 中的其他方法），因此它仍然可以支持此类库。
最后，根据我们的经验，在调试合成故障时，两种方法都相似。我们发现确定此类故障是否是由于 Sketch 的具体部分，漏洞和合成器或库模型（代数规范或模拟）而引起的，这是具有挑战性的。显然，改进合成调试是未来工作的有趣方向。我们期望代数规范和模拟都不会强烈地优于彼此，并且在 JLibSketch 中它们都将在同一系统中提供最大的帮助。
7 结论我们引入了 JLibSketch ，这是一个 Java 程序合成工具，可以在其中使用代数规范描述库方法。 JLibSketch 将其问题编译为 Sketch 问题，其中库方法返回 ADT 。代数规范被编译为重写那些 ADT 的函数。我们对汇编进行了形式化验证，证明了如果代数规范是有序且不可统一的，那么它是正确且完整的。我们针对来自三个领域的九个合成问题评估了 JLibSketch 。我们发现，与模拟相比，代数规格平均只有大小的一半，并且在九个问题中的七个问题上，可使合成速度提高 2 倍至 81 倍。因此，我们相信 JLibSketch 在推动库程序的合成实用化方面迈出了重要的一步。
8 致谢本文由南京大学软件工程系张皓明翻译转述。