仅从测试能否合成形式化规格说明？
Can Formal Specifications Be Synthesized from Tests Alone?
浏览论文内容
中文总结 AI 辅助
该研究提出仅用测试代码和动态执行轨迹，结合LLM与有界模型检查合成形式化规格说明的方法，在SpecGenBench基准上取得初步效果，同时指出需解决检查器兼容性等关键挑战。
中文摘要 AI 辅助
形式化规格说明能提供强保障，但手动编写成本高昂。近期基于大语言模型（LLM）的方法通过从源代码推断规格说明实现自动化，然而这类方法依赖白盒访问，因知识产权风险和部署成本阻碍了工业应用。本文提出的方法仅通过测试代码和动态执行轨迹，使用LLM推断候选规格说明：LLM仅能观察程序接口、选定输入及对应输出或状态变化，实现内部细节保持隐藏。采用有界模型检查在本地验证候选规格说明，反馈用于指导迭代优化。在SpecGenBench基准上的初步结果表明，测试可引导LLM生成有意义的Java建模语言规格说明，同时也凸显了检查器兼容性和诊断反馈是可靠优化的关键挑战。
英文摘要
Formal specifications offer strong guarantees, but remain costly to write manually. Recent LLM-based approaches automate this by inferring specifications from source code, yet their reliance on white-box access poses barriers to industrial adoption due to intellectual property risks and deployment costs. Our approach uses LLMs to infer candidate specifications solely from test code and dynamic execution traces: the LLM observes only the program interface, selected inputs, and corresponding outputs or state changes, while the implementation internals remain hidden. Candidate specifications are validated locally using bounded model checking, with feedback guiding iterative refinement. Initial results on the SpecGenBench benchmark suggest that tests can guide LLMs towards meaningful Java Modeling Language specifications, while also highlighting checker compatibility and diagnostic feedback as key challenges for reliable refinement.
