Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?

1 INTRODUCTION

• Natural-language documentation may diverge from implementation behavior, a concern heightened when AI-assisted programming generates code from user intent.Reliable translation to formal specifications could help catch bugs before production and improve trust in AI-generated code.Source: §1 · p. 2

1.1.1 Formalizing User Intent.

• For an ambiguous duplicate-removal description, two postconditions encode different readings, and only the second matches the programmer’s intent.The example illustrates how assertions can make competing interpretations explicit and checkable.Source: §1.1.1 · p. 2

1.1.2 Detecting Real-World Functional Bugs.

• GPT-4-generated postconditions caught a historical Commons Math bug in which a reversed Line object lacked sufficient precision.The example’s postconditions use project context and mathematical knowledge about reversed lines.Source: §1.1.2 · p. 3

1.2 Overview

• The study asks whether LLM-generated postconditions formalize informal intent and whether they can catch real-world bugs, evaluating both questions across benchmarks and programming languages.The evaluation combines automated correctness and completeness metrics, prompt variants, and quantitative and qualitative analyses.Source: §1.2 · p. 4

1.3 Contributions

• LLMs generated postconditions that detected 64 historical bugs in industrial-scale Java projects, with correct postconditions on EvalPlus reaching 96% of problems and discriminating up to 81% of buggy programs on average.The paper frames these results as evidence that sufficiently robust natural-language descriptions can support postconditions with high discriminative power.Source: §1.3 · p. 4

2.1 Problem formulation and metrics

• A candidate postcondition is an assertion over a method’s input and output states; the reference implementation and test inputs support offline evaluation, while tests are hidden from the generating LLM.The formulation assumes deterministic reference code and that each test input assigns values to the inputs and globals.Source: §2.1 · pp. 4–5, §2.1.1 · p. 5

2.1.1 Test-set correctness.

• A postcondition is test-set-correct when it evaluates true on the reference implementation’s output for every test input; accept@k estimates the chance that a sampled subset contains at least one such condition.The authors treat test coverage as a pragmatic approximation of all legal inputs.Source: §2.1.1 · p. 5

2.1.2 Test-set completeness for code mutants: bug-completeness-score.

• Bug completeness measures the fraction of distinct code mutants rejected by a correct postcondition on at least one test, using LLM-generated mutants rather than fixed mutation operators.The authors argue that fixed operators may miss bugs farther from the reference or written using different syntax or APIs; the metric depends on the mutant set’s coverage.Source: §2.1.2 · pp. 5–6

2.2 Prompt Design for LLM-based Postcondition Generation

• Prompt variants cross reference-code inclusion with requested complexity, producing four combinations; the simple prompt asks for an aspect of a function rather than the whole function.The default omits reference code, while an alternative includes it; the authors report that complex postconditions are more likely to be incorrect.Source: §2.2 · pp. 6–7

• The study assesses LLM-generated postconditions’ ability to capture and formalize intent through a detailed empirical evaluation on a popular benchmark.Source: §3 · p. 7

3.1.1 Evaluation Benchmark.

• EvalPlus contains 164 Python problems with docstrings, reference implementations, and validation tests, averaging 775 tests per problem.The benchmark extends HumanEval with a more extensive test suite.Source: §3.1.1 · pp. 7–8

3.1.2 Large Language Models.

• The study uses GPT-3.5, GPT-4, and StarChat, including both closed-access and open-access chat models.StarChat permits replication and comparison using the same prompt as the OpenAI models.Source: §3.1.2 · p. 8

3.1.3 Postcondition Generation.

• For each EvalPlus problem and LLM model, the authors generated 10 postconditions for each of four prompt variants, totaling 19,680 postconditions across all variants, models, and problems.They used a temperature of 0.7.Source: §3.1.3 · p. 8

3.1.4 Code Mutant Generation.

• Buggy-code mutants came from GPT-3.5-generated solutions that failed tests, including solutions prompted to contain errors; only mutants with distinct test-failure behavior were retained.The resulting unique-mutant counts ranged from 4 to 233 per problem, with a median of 55.Source: §3.1.4 · p. 8

3.2.1 Postcondition Correctness.

• 77% of postconditions were test-set-correct, and a correct postcondition was generated for 96% of problems (158/164) in the best-performing prompt variation.The authors report that EvalPlus test-set correctness largely corresponds to true correctness.Source: §3.2.1 · p. 9, Table 1 · p. 9
• GPT-4 postconditions had the highest accept@1 (0.63–0.77), followed by GPT-3.5 (0.46–0.56) and StarChat (0.21–0.25).StarChat generated at least one correct postcondition for 78%–86% of benchmark problems, depending on the prompt.Source: §3.2.1 · p. 9
• Simple prompts significantly increased correctness over base prompts (p=0.008; Cohen’s d=1.73).The paired comparison varied prompt complexity type; the authors recommend simpler postconditions when prioritizing correctness.Source: §3.2.1 · p. 9
• Including a reference solution did not significantly change correctness compared with using natural-language specifications alone (p=0.42).The authors suggest natural language alone may suffice when it is comprehensive enough.Source: §3.2.1 · p. 9

3.2.2 Postcondition Completeness.

• GPT-4 postconditions were bug-complete for up to 62.2% of EvalPlus examples, with average bug-completeness scores up to 0.85 for GPT-4 and 0.76 for GPT-3.5.Bug-completeness measures whether postconditions detect buggy code mutants; the authors report that these models’ average correct postconditions discriminated over three-quarters of unique mutants.Source: §3.2.2 · p. 10, Table 2 · p. 11
• Base prompts generally achieved higher bug-completeness scores than simple prompts, while simple GPT-4 and GPT-3.5 postconditions still discriminated over half of unique buggy mutants.Reference-solution prompts had a nonsignificant 5% higher average bug-completeness score (p=0.06), which the authors associate with more functional re-implementations.Source: §3.2.2 · p. 10
• Completeness scores were consistently, though not always substantially, lower for natural bugs than artificial bugs, which can inflate the metric; generating unique natural bugs is more expensive.The authors suggest augmenting evaluation with artificial bugs may still be useful for metric robustness.Source: §3.2.2 · pp. 10–11

3.2.3 Qualitative Analysis of Generated Postconditions.

• The qualitative analysis classified nine atomic property types and found that 33% of postconditions conjoined multiple properties with &&.Prevalence is counted across atomic and conjoined statements, so category percentages can sum to over 100%.Source: §3.2.3 · pp. 11–12

4 RQ2: CAN NL2POSTCOND HELP CATCH REAL WORLD BUGS?

• The study investigates nl2postcond’s potential for finding bugs in existing code.This is the paper’s second motivating use case.Source: §4 · p. 13
• The evaluation uses Defects4J, a benchmark of historical Java bugs.Source: §4 · p. 13
• The focus is on whether generated postconditions can find bugs in an existing code base.Source: §4 · p. 13

4.1.1 Benchmark: Defects4J.

• Defects4J 2.0 provides 835 manually curated bugs from 17 Java projects, with buggy and fixed versions and trigger and regression tests.The Java 8 subset contains 525 reproducible bugs affecting 840 functions.Source: §4.1.1 · p. 13

4.1.2 Bug Discriminating Postconditions.

• A postcondition is bug-discriminating when it passes all trigger and regression tests on the fixed function but fails at least one on the buggy function.Because Defects4J minimizes changes to the bug fix, the authors treat a discriminating postcondition as related to that change, assuming comprehensive tests.Source: §4.1.2 · p. 13

4.1.3 Prompt Design and Ablations.

• For Defects4J, the authors add class and type context and greedily include call-graph methods until the model’s context window is exhausted.They use in-file comments, primarily JavaDoc, as the natural-language specification and do not add generated summaries or external documentation.Source: §4.1.3 · p. 14
• The study tests two prompt variants with GPT-4 and StarChat, generating 10 postconditions for each of 840 functions.The variants use natural language alone or natural language plus the buggy function body; the selected simple prompt performed better for correctness in RQ1.Source: §4.1.3 · p. 14

4.2 RQ2–Results: can LLM-generated postconditions catch real-world bugs?

• The study reports both high test-set correctness and bug-discriminating postconditions for a subset of real-world Defects4J bugs.Source: §4.2 · p. 14

4.2.1 Test-set correctness.

• GPT-4 achieved test-set correctness of accept@1 up to 0.39 and accept@10 up to 0.75, while StarChat achieved 0.12 and 0.56, respectively.These are results for postconditions checked against the fixed version; including buggy code in the prompt generally increased correctness.Source: §4.2.1 · pp. 14–15

4.2.2 Bug-discriminating postconditions.

• Across all prompt variants and models, the study generated bug-discriminating postconditions for 70 buggy methods from 64 unique Defects4J bugs, representing 12.2% of all 525 bugs considered.GPT-4 generated discriminating postconditions for up to 47/525 bugs (9%); StarChat distinguished up to 25 bugs.Source: §4.2.2 · p. 15

4.2.3 Qualitative analysis of bug-discriminating postconditions.

• In the CLI example, GPT-4 generated postconditions that catch a rendering bug where padded lines exceeded the documented width.The bug-catching postconditions came from both prompt variants.Source: §4.2.3 · p. 15, Figure 5 · p. 16
• For a Commons Math reversed-line bug, GPT-4 generated postconditions that detect insufficient precision in the returned object’s internal state.Both example postconditions were generated with the buggy code included; one combines a project method with external algebraic knowledge.Source: §4.2.3 · pp. 15–16

4.3.1 TOGA.

• Unlike TOGA’s test-prefix assertions, nl2postcond generates method postconditions expected to hold for all inputs.TOGA assertions apply at testing time to the specific prefix reaching the buggy location; method postconditions can also be checked at runtime on unseen inputs.Source: §4.3.1 · pp. 16–17
• Of 101 bugs caught by TOGA or nl2postcond, only 5 were caught by both; 59 were caught only by nl2postcond and 37 only by TOGA.The authors characterize the approaches as complementary.Source: §4.3.1 · p. 17
• TOGA could not find 52 of nl2postcond’s 64 bugs because no EvoSuite test prefix reached the bug location.Many TOGA-caught bugs involved exceptional behavior, which nl2postcond did not model in this evaluation.Source: §4.3.1 · p. 18

4.3.2 Daikon.

• Daikon produced a bug-discriminating postcondition in only three instances, and two of those specifications were incorrect because they overfit regression tests.Daikon generated invariants for 78 of 101 tested bugs, but some were weak or timed out.Source: §4.3.2 · p. 19

4.3 Baseline comparison: TOGA, Daikon

• Across the comparison, nl2postcond was more widely applicable or found more bugs than TOGA and Daikon; its bug catches were largely non-overlapping with TOGA’s.Daikon usually generated invariants that overfit observed executions.Source: §4.3.2 · p. 19

5 RELATED WORK

• nl2postcond infers desired code behavior from natural language, unlike most existing specification-inference work that derives specifications from implementations.Prior documentation-based methods often rely on handcrafted rules and heuristics.Source: §5 · p. 19
• Earlier documentation-based approaches often require semi-structured input and transfer poorly across languages and domains, while this technique was evaluated in Python and Java.The approaches use techniques such as pattern matching, text normalization, entity recognition, and parsing.Source: §5 · p. 20
• Unlike concrete test-generation approaches such as AthenaTest [49] and TiCoder [23], nl2postcond targets abstract input-output relationships; unlike EvoSpex [32], it specifies desired rather than existing behavior.The paper also distinguishes its correctness and completeness evaluation from Speculyzer [21], which uses likely properties and inputs as code-generation heuristics.Source: §5 · p. 20

6 LIMITATIONS AND THREATS TO VALIDITY

• Using black-box LLMs limits interpretability and raises generalizability questions, while the fast-changing AI landscape may make results obsolete quickly.These are described as inherent weaknesses of the approach.Source: §6 · p. 20
• EvalPlus and Defects4J may have appeared in training data for StarChat, GPT-3.5, or GPT-4, threatening internal validity; the authors note postconditions are not artifacts of those datasets.They know of no public-facing dataset that previously generated postconditions.Source: §6 · p. 20
• OpenAI web APIs may be updated or deprecated, threatening replicability; the authors share generated artifacts and also use open-access StarChat.They report accept@k to account for stochastic model output.Source: §6 · pp. 20–21
• Findings may not generalize beyond the 525 Defects4J bugs, languages, and repositories studied; the EvalPlus-derived postcondition taxonomy may also not extend across languages or program complexities.The authors partly mitigate this concern by evaluating real-world bugs and both Python and Java benchmarks.Source: §6 · p. 21
• The completeness measure depends on mutant coverage: generated mutants cannot comprehensively represent all possible bugs, despite retaining distinct mutants and generating up to 233 buggy codes per problem.The authors identify this dependence as a threat to internal validity.Source: §6 · p. 21

7 CONCLUSION

• LLM-generated postconditions discriminated 64 real-world historical bugs from industrial-scale Java projects.The authors also find that generated postconditions are generally correct and capture programming intent.Source: §7 · p. 21
• The paper introduces nl2postcond and proposes and validates metrics for assessing the correctness and completeness of natural-language-derived postconditions.The authors describe this as an initial step in systematizing the problem.Source: §7 · p. 21
• The findings support the feasibility of turning natural-language documentation into executable specifications for software validation and bug detection.The paper characterizes LLMs as a promising bridge between informal descriptions and formal code specifications.Source: §7 · p. 21

8 DATA AVAILABILITY

• The planned replication package includes generation scripts and prompts, an evaluation harness, a qualitative codebook, generated postconditions, temperature ablations, and unique EvalPlus mutants.The authors describe these releases as planned for the near future.Source: §8 · p. 21