Traditional formal specification generation methods are typically tailored to specific specification types, and therefore suffer from limited generality. In recent years, large language model (LLM)-based specification generation approaches have emerged, offering a new direction for improving the universality of automated specification synthesis. However, when dealing with complex control flow, LLMs often struggle to precisely generate complete specifications that cover substructures. Moreover, the distinctive verification pipelines adopted by existing approaches may incorrectly discard logically correct specifications, while verification tools alone cannot reliably identify correct specifications. To address these issues, we propose SLD-Spec, an LLM-based specification generation method that combines program slicing and logical deletion. Specifically, SLD-Spec augments the conventional specification generation framework with two key stages: (1) a program slicing stage that decomposes the target function into several smaller code slices, enabling LLMs to focus on more localized semantic structures and thereby improving specification relevance and completeness; and (2) a logical deletion stage that leverages LLMs to perform logical reasoning and filtering over candidate specifications so as to retain logically correct ones. Experimental results show that SLD-Spec consistently outperforms existing methods on datasets containing programs of varying complexity, verifying more programs and generating specifications that are more relevant and more complete. Further ablation studies indicate that program slicing mainly improves specification relevance and completeness, whereas logical deletion plays a key role in increasing verification success rates.

翻译：传统的形式化规约生成方法通常针对特定规约类型定制，因此普遍性有限。近年来，基于大语言模型（LLM）的规约生成方法兴起，为提升自动化规约合成的通用性提供了新方向。然而，在处理复杂控制流时，LLM往往难以精确生成覆盖子结构的完整规约。此外，现有方法采用的独特验证流程可能错误地丢弃逻辑正确的规约，而仅靠验证工具无法可靠识别正确规约。为解决这些问题，我们提出了SLD-Spec，一种结合程序切片与逻辑删除的基于LLM的规约生成方法。具体而言，SLD-Spec在传统规约生成框架中增加了两个关键阶段：（1）程序切片阶段，将目标函数分解为若干较小的代码切片，使LLM能够专注于更局部的语义结构，从而提升规约的相关性与完整性；（2）逻辑删除阶段，利用LLM对候选规约进行逻辑推理与过滤，以保留逻辑正确的规约。实验结果表明，在包含不同复杂度程序的数据集上，SLD-Spec始终优于现有方法，能够验证更多程序并生成相关性更强、更完整的规约。进一步的消融研究表明，程序切片主要提升规约的相关性与完整性，而逻辑删除则在提高验证成功率方面发挥关键作用。