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

当 JLibSketch 在此示例上执行合成时，它使用图 2a 中的规则为 TreeSet 方法赋予语义。例如，图 2c 底部的注释显示了 testLRS 发生的重写步骤，为简单起见，假设 JLibSketch 已达到正确的解决方案。请注意，实际上， JLibSketch 在合成过程中执行重写，因此，所采取的重写步骤取决于漏洞和合成器，而控制取决于控件，并且以重写方式表示的数据值还可以包括漏洞和合成器。
在此特定示例中，使用代数规范具有明显的优势。代数规范大约是模拟代码行数的一半，并且与模拟相比，代数规范的运行速度至少要快两倍。在我们的实验中，我们发现这种趋势在其他情况下同样成立。另一个潜在的好处是，使用代数规范描述方法之间的关系可能比描述方法本身更简单。例如，如引言中所述，我们可以编写代数规范，例如 crypto(encrypt(m,k),k)?m ，而无需提供加密或解密的实际实现。
4 编写 Sketch 代数规范JLibSketch 遵循与 JSketch 相同的方法，该方法是将 JSketch 问题编译为 Sketch 问题，在结果上运行 Sketch ，然后将 Sketch 的解决方案映射到原始 JSketch 输入。
为了简化形式推理，我们从概念上将 JLibSketch 的编译过程分为两个步骤。第一步将 JLibSketch 编码为 Sketch + lib core ，这是我们介绍的一种核心语言，类似于 Sketch ，并已内置了对代数规范的支持。
文章插图
图 3 Sketch+lib core 的语法和 Sketchcore
图 3 给出了我们的核心语言的语法。突出显示的部分仅是 Sketch + lib core 的一部分，我们将在下面进行讨论。
【代数库规范下的程序合成】在 Sketchcore 中，程序 P 由一组代数数据类型声明 A ，一组线束 H ，以及一组空的重写规则 E 。线束的主体是语句序列。赋值 z:= E 将原始变量 z 绑定到表达式，表达式可以是原始值， holes？原始变量或表达式的和或差。给定具有常规连接词的布尔表达式，假定和断言语句的行为符合预期。分配 d:= R 将 ADT 变量 d 绑定到 ADT 项。在语句 d:= match(d,R) ， d 是 ADT 变量， R 是模式，即带有一组变量的 ADT 项。如果 d 表示的项可以与模式 R 匹配，则 R 中的每个变量都将映射到 d 的子项。这些子项可以通过它们在模式 R 中的位置（从左到右）进行排序，并绑定到 ADT 变量 d 的向量上。请注意， Sketchcore 不包含分支或循环。假设所有循环都是有界的（在 Sketch 中就是这种情况），则可以使用假定将这些形式分为多个直线线束。
为了将 Sketchcore 扩展到 Sketch + lib core ，我们引入了库函数 f 。这样的函数可以返回原始值或库值 u 。请注意，后者永远不会出现在表面语法中，因为只能通过调用库函数来创建它们。为简单起见，我们假定库函数仅返回一种库类型。
我们从句法上区分可以保存库类型值的库变量 x 和原始变量，并允许在条件位置的库变量之间进行相等性测试。然后，我们将语句语言扩展为包括两个库调用分配：z:= f(Vˉ)和 x:= f(Vˉ) ，它们分别将原始变量和库变量绑定到库调用的结果。此类调用的参数是变量序列；可以通过首先将它们分配给变量来传递值。最后，我们以重写 T?T'的形式介绍重写规则，其中术语 T 和 T'是由原始/库值，原始/库变量，库调用和原始操作组成的模式。我们为 T 的自由变量写 Vars(T) ，并假设如果重写 T?T'是规则，则 Vars(T')?Vars(T) 。我们将这样的规则解释为意味着实例化 T 的任何表达式都等效于实例化 T'的相应（简化）表达式。
要定义合成问题，我们首先需要描述如何使用重写规则运行程序。为了简化我们的语义，我们假设存在对库调用进行建模的 Orcl 。更具体地说，对于每个函数 f(v) ， Orcl 将自变量 v 映射到返回值[f(v)]Orcl 。
定理 1：如果对于所有 t 和 t'满足[t]Orcl = [t']Orcl ，则 Oracle Orcl 是一个 E 模型，以便可以使用 E 中的规则将 t 重写为 t' 。
现在，我们可以为 Sketch + lib core 定义一个语义。对于线束主体，我们的语义证明了以下形式的判断：?Env,S?Orcl→?Env',S'? ，这意味着在初始环境 Env 中，使用 Orcl 执行语句 S 会产生环境 Env' ，其余的语句 S'将被执行，而没有任何断言冲突。断言冲突减少为 F 中的特殊错误项。最后在线束中，评估线束使用其参数的任意绑定来评估其主体。完整的语义可以在附录 A 中找到。有了这种语义，我们现在可以定义合成问题：给定 Sketch + lib core ，找到漏洞的解决方案，以便在任何执行中都没有断言。