一句话：提出 Barista，用 LLM 智能体从文档合成 typestate 规约，实现 Java 对象协议的编译期验证。
面向对象类隐含客户端必须遵守的对象协议，如先连接套接字再发送数据，主流语言无法在编译期校验。已有 typestate 系统能检测违规，但需人工形式化协议。本文提出 Barista：一种结合 LLM 与测试生成的智能体工作流，通过 DFA 引导从类文档提取对象协议，合成 LiquidJava 规约，并以测试合成和验证驱动精化迭代修正。在 35 个 Java 类上以专家标注为基准，达到 87.0% 精确率与 68.3% 召回率，75% 规约可直接使用或仅需少量编辑，降低了人工标注负担，使编译期协议安全更易获得。
Object-oriented classes encode implicit protocols that clients must follow, such as connecting a socket before sending data or opening a stream before reading. Mainstream programming languages like Java cannot validate the correct use of these protocols, but more advanced type systems, such as typestate systems, can detect these violations at compile time. However, these systems require a formalization of these implicit protocols. To overcome this limitation, we propose to extract object protocols from documentation using a combination of LLMs and test generation. We developed Barista, an agentic workflow that transforms class documentation into verifiable LiquidJava specifications through DFA-guided protocol extraction, test synthesis, and verification-driven refinement. We evaluated our approach on 35 Java classes with expert-written ground truth, achieving 87.0% precision and 68.3% recall, with 75% of specifications usable directly or with minor edits. Barista bootstraps these specifications for well-documented libraries, reducing the manual annotation burden and enabling compile-time protocol safety without specialized expertise.
@inproceedings{paperbot12441,
title = {Barista: Synthesizing Typestate Specifications with LLM Agents},
author = {Catarina Gamboa and Paulo Canelas and Ricardo Costa and Márcio Caetano and Jonathan Aldrich and Alcides Fonseca},
booktitle = {ASE},
year = {2026},
doi = {10.1145/3832783.3834427}
}