大型语言模型（LLM）在从源代码合成形式化规范方面展现出显著潜力。现有方法主要聚焦于函数合约和循环不变式，往往忽视帧条件——即在执行期间可能被修改或保持不变的内存位置，这在形式化规范中至关重要。\ \ 本文提出一种基于 LLM 的方法，能够在 C 代码中同步生成 ACSL 帧规范和函数合约。核心思路是先利用代码属性图（CPG）抽取与帧相关的信息，包括变量的作用域、指针别名以及可能的写入路径。随后将这些结构化信息作为提示注入 LLM，指导其生成符合实际修改行为的帧条件。\ \ 生成的规范同时捕获区域分离约束和数据依赖关系，明确哪些内存块在函数调用后保持不变，哪些会被更新。\ \ 实验在两个基准上评估方法效果。第一个基准包含 84 个符合 ACSL 的真实系统函数，方法成功合成无错误帧规范的比例达到 92.9%，相较于最先进技术提升了 179%。第二个基准包含 51 个函数，成功率从 80.4% 提升至 96.1%。将本方法作为辅助模块嵌入现有 LLM‑ACS L 合成框架后，帧规范生成性能最高提升 61.9%。\ \ 点评：该工作通过结合代码属性图与大语言模型，有效弥补了自动规范合成中对帧条件的缺失，为形式化验证提供了更完整的规格描述。