为什么类型状态规范一直很难写

写过 API 的人大概都遇到过这种坑：某个对象必须先调用 open() 再调用 read()，顺序错了就崩。这类「调用顺序」的约束，在编程语言理论里叫类型状态（typestate）规范。它描述的不是「这个变量是 int 还是 string」，而是「这个对象现在处于哪个生命周期阶段，允许你做什么操作」。

问题在于，类型状态规范写起来非常费劲。它要求开发者手动列出所有状态、所有合法迁移、所有非法操作，还要保证规范和真实代码行为一致。现实项目里，大多数人干脆不写，靠文档和 code review 兜底，于是 bug 就藏在「顺序错了」这种地方。

Barista 这篇论文想解决的就是这个痛点：能不能让 LLM Agent 自动把类型状态规范推出来？

Barista 的基本思路

Barista 的核心主张是：LLM 已经读过大量代码和文档，它对「某个 API 应该怎么用」其实有相当强的先验知识。与其让人从零手写状态机，不如让 Agent 去读代码、读用法、读测试，然后生成候选规范，再用程序分析工具去验证和修正。

它把整个任务拆成一个循环：

1. 观察：Agent 读取目标代码库，包括函数签名、调用点、注释和测试用例。
2. 假设：Agent 基于这些信息，提出一个初始的类型状态规范，比如「状态 A 下只能调用 init，调用后进入状态 B」。
3. 验证：把候选规范交给静态分析或运行时检查，看它是否和现有代码冲突。
4. 修正：如果出现反例，Agent 根据反例调整规范，回到第 2 步。

这个循环的关键在于：LLM 负责「猜」，形式化工具负责「证伪」。LLM 单独用容易幻觉，形式化工具单独用又需要人喂规范，两者结合刚好互补。