SLICE：合同执行的规范级隔离

编程问题通常指定函数应执行的计算及其输入必须满足的条件。 大语言模型 被广泛用于从这些问题规范生成代码，并且生成的函数必须在执行规定的输入条件的同时实现所需的计算。规定的投入条件共同构成投入合同。执行此合同很困难：不完整的执行接受应拒绝的输入，而过度限制性的执行则拒绝应接受的输入。现有的代码生成方法没有提供识别输入契约和功能需求并生成共同满足它们的代码的生成过程。因此，我们引入了 SLICE，这是一个生成框架，它可以识别这两个需求并通过单独的生成阶段来解决它们。 SLICE 由三个阶段组成：（i）基于图的规范构建，它将合同条件建立在规范图中的描述部分，并删除仅合同部分以形成功能视图； (ii) 函数体生成，通过贪婪和采样解码产生多个候选函数体，使用执行分数对它们进行排名，并使用差异区域对数概率解决关系； (iii) 合约断言生成，根据已识别的合约条件生成输入验证断言并将其附加到选定的函数体。我们在四个 LLM 上评估 ContractEval 上的 SLICE，并将其与六种竞争方法进行比较。相对于每个模型的最强评估基线，SLICE 在生成满足功能要求和输入契约的代码方面的性能平均提高了 6.58%。我们的代码可在 https://github.com/suhanmen/SLICE 获取。