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

定理 2：如果可以为 H 中的每个漏洞分配一个值以形成不带漏洞的线束 H' ，则 Sketch + lib core 程序 P = A;H;E 有效。
定理 3：令 T 为整数理论（Sketchcore 中的基元）。对于任何 Sketch + lib core 程序 P = A;H;E ，当且仅当 T∪E | =?hˉ.VC(P(h))时，程序 P 才有效。这里 T∪E | = ? 表示 ? 假设理论 T 和 E 中的重写规则。
定理 4：如果没有无界序列 φ1→E, φ2→E, φ3→E ，则终止一组重写规则 E 。
定理 5：每当 Φ→E?ψ 和 Φ→E?ψ'存在一个 θ 使得 ψ→E?θ 和 ψ'→E?θ 时，一组重写规则 E 是适用的。
定理 6：一个有序且不可统一的重写系统是会终止并且融合起来的。
定理 7：给定任何公式 φ 的终止和汇合重写规则 E ，存在一个唯一的公式 ψ ，使得 φ→E?ψ 和 ψ 不再可以重写。我们将 ψ 称为 φ 的规范形式，并将其表示为 CanE(φ) 。
最后，我们可以使用规范的形式来转换关于库函数的推理，这种形式是唯一的并且可以确定地计算：
定理 8：令 E 为终止和融合的重写规则集，然后对于任何 φ ，当且仅当 T|= CanE(φ)时， T∪E | =φ 。
我们定义了一个从 Sketch + lib core 到 Sketchcore 的编译器 J_KE ，它采用以下步骤：
（1）标准化 PTO 单一静态分配（SSA）形式，即对于程序中的每个分配，为变量的每次更新引入一个新的新变量，并相应地重命名该变量的所有用法。
（2）对于每个语句 assume(φ)或 assert(φ) ，将每个非输入变量重复替换为该变量唯一赋值的右侧，直到所有变量均为输入变量为止。
（3）对于每个剩余的条件 assume(φ)或 assert(φ) ，将其替换为 assume(CanE(φ))或 assert(CanE(φ)) 。
刚刚描述的编译器假定我们可以在编译期间计算规范形式，但是如果执行依赖于未知数，则通常是不可能的。为此，我们将术语表示为 ADT ，然后通过对 ADT 进行操作来模拟术语重写。为此，我们需要一个略微扩展的 Sketchcore 版本，其中包括 ADT ，模式匹配和条件。
图 4 显示了一些合成的 ADT 代码。在图的顶部，我们创建了一个 ADTF ，它表示返回非基本值的库调用项。对于基本类型的整数，我们为返回整数的库调用创建 ADT I ，并为带有 ADTB 的布尔值创建 ADTI 。图的底部显示了对重写规则进行编码的重写函数。它通过执行案例分析来工作，每个案例都尝试匹配规则左手边的模式，并用相应的右手边替换。第一组测试将重写处理到术语的最高级别，而 switch 语句则处理嵌套的重写。这个特殊的重写函数处理返回库类型的情况。通过这种 ADT 嵌入，我们可以将 Sketch + lib core 程序 P 编译为 Sketchcore 程序 JPKAEDT 。因此可见，将重写规则编译为 ADT 操作是正确且完整的。
文章插图
图 4 ADTs 和重写函数的定义
5 实现开发 JLibSketch 的两个主要挑战：在 Sketch 内部实现重写功能，并引入装箱以允许 Java 原语和对象在必要时进行混合。
在 Sketch 中实现 JLibSketch 重写：通过使用 Sketch ADT 编码@rewriteClass 方法并通过 ADT 重写模拟术语重写来工作。
装箱基元和数组：在 JLibSketch 中，通过代数指定的返回值的库方法可以通过重写产生一些实际值，或者可以评估为 ADT ，直到以后与其他方法调用结合使用。由于 ADT 以 Object 类型存储（图 5），因此对于返回对象的库方法来说，这很好用。但是，在 Java 中，基元不是对象。为了解决此问题， JLibSketch 要求用户注释必须装箱的位置，以便原语/数组和对象可以同时出现，以及应拆箱的位置，以允许在使用前访问值。
文章插图
图 5 Sketch 部分代码
6 实验我们通过比较使用代数规范的合成与使用模拟在一组 Java 程序上进行的合成来评估 JLibSketch 。我们的基准套件由来自 GitHub 的九个客户端程序组成，来自三个应用程序领域：数据结构，密码学和文件操作。我们修改了每个基准，通过引入漏洞和合成器将其转换为合成问题。表 1 的前三列以代码行（LoC）的形式给出了大小，并简要介绍了每个基准。
表 1 使用 LoC 比较模拟和重写的客户端程序
文章插图
我们根据方法的文档开发了代数规范，这对于我们的目标库而言非常清楚。我们已经在图 2a 中看到了一些示例代数规范。为了验证重写终止，我们确认规则是有序的，即无法通过应用一系列规则来重写术语，并检查规则是否不可统一，即在任何情况下都不会可能会触发一条规则，或者一条规则的模式可能与另一条规则重叠。为了开发模拟程序，我们查看了相同的文档，并编写了简单，直接的实现方式并且有效。