LM2Alloy：大模型生成形式规约并推导生产软件测试

我们提出了一项探索性研究，使用 大语言模型 (LLM) 从需求文档和生产源代码生成 Alloy 形式规范，并从这些规范中导出可执行测试用例。我们评估了两个真正的开源 Python 库：Flipper（功能标志管理系统）和 Cerberus（数据验证库）。在这两种情况下，LLM 都生成了可行的Alloy规约和可执行测试，无需任何手动校正。对于 Flipper，我们的管道发现了现有测试套件遗漏的一个真正的错误：该库默默地接受重复的标志名称，直接违背了其记录的唯一性要求。直接的 LLM 基线（从相同的 README 生成测试但跳过 Alloy 步骤）实现了 68% 的分支覆盖率，但未能在所有三个独立运行中捕获此错误。这表明引入形式化的中间表示可以暴露面向覆盖的生成可能错过的约束级别缺陷。对于 Cerberus，代码派生的规范捕获了文档派生的规范忽略的大小类型的隐式抽象，从而产生了两个额外的测试。在这两个库中，基于代码的规范在测试生成方面的方差（平均 SD = 2.15）低于基于文档的规范（平均 SD = 5.0），尽管这是否具有普遍性仍然是一个悬而未决的问题。索引术语——形式化规范、Alloy、大语言模型、自动化测试、规范漂移、软件验证。