Formal specifications play a central role in ensuring software reliability, yet automatically synthesizing high-quality specifications remains difficult and often requires domain expertise. Recent work has applied large language models to generate specifications in the Java Modeling Language (JML), reporting high verifier pass rates. But passing a verifier only confirms that an implementation is consistent with a specification, not that the specification is meaningful: a trivial postcondition such as ensures true satisfies any verifier while saying nothing about the code. Mutation-based completeness scores go further, but they return a single number and cannot tell a generator which clause to fix. In this work, we first compare classical and prompt-based JML synthesis under a unified setup, and find that 22.7% of the verified specifications have no postcondition at all, and that prompt optimization through verification feedback repairs weak prompts but does not go beyond the best hand-written one. We then introduce Spec-Harness, a framework that measures the behavioral adequacy of a specification along four dimensions of precondition and postcondition correctness and completeness, using Hoare-triple based symbolic verification and input/output mutation on systematically built test suites. Spec-Harness reveals that many verifier-accepted specifications are behaviorally weak, over- or under-constraining inputs and outputs in ways the verifier cannot see. Finally, we show that Spec-Harness works as a feedback signal that helps coding agents synthesize specifications with higher behavioral adequacy on held-out tests. This holds for the general-purpose agents Codex and Claude Code and for a CodeAct-style JML synthesis agent that we built to use the verifier and Spec-Harness as feedback.

翻译：暂无翻译