# Formalizing Natural Language Intent into Program Specifications via Large
Language Models

Madeline Endres  University of MichgainAnn ArborMIUSA<EMAIL_ADDRESS>,
Sarah Fakhoury  Microsoft ResearchRedmondWAUSA<EMAIL_ADDRESS>,
Saikat Chakraborty  Microsoft ResearchRedmondWAUSA<EMAIL_ADDRESS>and
Shuvendu K. Lahiri  Microsoft ResearchRedmondWAUSA<EMAIL_ADDRESS>
###### Abstract.

Informal natural language that describes code functionality, such as code
comments or function documentation, may contain substantial information about
a program’s intent. However, there is typically no guarantee that a program’s
implementation and natural language documentation are aligned. In the case of
a conflict, leveraging information in code-adjacent natural language has the
potential to enhance fault localization, debugging, and code trustworthiness.
In practice, however, this information is often underutilized due to the
inherent ambiguity of natural language which makes natural language intent
challenging to check programmatically. The ”emergent abilities” of Large
Language Models (LLMs) have the potential to facilitate the translation of
natural language intent to programmatically checkable assertions. However, it
is unclear if LLMs can correctly translate informal natural language
specifications into formal specifications that match programmer intent.
Additionally, it is unclear if such translation could be useful in practice.

In this paper, we describe LLM4nl2post, the problem leveraging LLMs for
transforming informal natural language to formal method postconditions,
expressed as program assertions. We introduce and validate metrics to measure
and compare different LLM4nl2post approaches, using the correctness and
discriminative power of generated postconditions. We then perform qualitative
and quantitative methods to assess the quality of LLM4nl2post postconditions,
finding that they are generally correct and able to discriminate incorrect
code. Finally, we find that LLM4nl2post via LLMs has the potential to be
helpful in practice; specifications generated from natural language were able
to catch 70 real-world historical bugs from Defects4J.

##  1\. Introduction

Informal natural language specifications are omnipresent in modern software.
For example, Pfeiffer (Pfeiffer, 2020) found natural language documentation in
98% of over 20,000 GitHub repositories, with 10% of repository artifacts
specifically for documentation. He (He, 2019) found over 20% of non-blank
program lines contained in-file comments in their study of 150 of the most
starred projects on GitHub. At the same time, it is well known that software
bugs (unexpected exceptions, incorrect output) often arise from the weak
association between the intended behavior (documented in natural language) and
the behavior of the implementation (Tan et al., 2007, 2012). This issue is
exacerbated with AI-assisted programming where users generate code from
natural language intent (GitHub, 2023; AWS, 2023; Tabnine, 2023), without a
good way to ensure their association. Reliably translating informal natural
language descriptions to formal specifications could help catch bugs before
production and improve trust in AI-generated code (Lahiri et al., 2022).

Current approaches to translating natural language descriptions to formal
specifications are heuristic-based and either rely on the input being in a
structured format (Blasi et al., 2018; Tan et al., 2012) or can only generate
a fairly restricted class of specifications (e.g., regarding nullness or
exceptions or locking rules) (Goffi et al., 2016; Tan et al., 2007; Su et al.,
2023). Further, most of these approaches work for a specific programming
language (such as Java), given their customized nature. In the past, large-
scale neural modeling for the problem of generating specifications has been
difficult given the absence of large code corpora with matching natural
language intent and corresponding specifications.

Large Language Models (LLMs) have generated a lot of interest in the area of
programming owing to their ability to synthesize high-quality natural code
from natural language intent in a surrounding context (Chen et al., 2021;
Nijkamp et al., 2022; Li et al., 2023). Given the limitations of the current
approaches for translating natural language to specifications, we explore the
use of LLMs for the problem of translating informal intent to formal
specifications. Even though these LLMs have not seen structured data matching
natural language intent to specifications, larger models such as GPT-4 have
demonstrated ”emergent abilities” to do well on tasks that they were not
explicitly trained for, or unlikely to be common in the training corpus (Wei
et al., 2022). In particular, models such as GPT-4 demonstrate capabilities to
follow natural language instructions to perform reasoning tasks, for example,
through emergent prompting strategies like few-shot learning (Lampinen et al.,
2022), chain-of-thought (Wei et al., 2023) and multi-step reasoning (Zhou et
al., 2023). In particular, we explore the feasibility of leveraging LLMs to
act as a usable and practical bridge between informal natural language and
useful method postconditions. We assess this ability in a programming
language-agnostic way, by targeting postconditions that can be expressed as
assertions in the underlying programming language. We term this approach as
LLM4nl2post — leveraging LLMs for the purpose of translating natural language
method-level comments to corresponding postconditions. A postcondition for a
method is an assertion that relates the input and output states of the method,
and holds true after any successful execution of the method.

Let us motivate the approach using a couple of motivating examples.

###  1.1. Motivating Examples

####  1.1.1. Formalizing User Intent

Consider the example in Figure 1, taken from the popular Python code
generation benchmark, HumanEval (Chen et al., 2021). A programmer intends a
function to remove from a given list all numbers that have duplicates. For
example, given a list containing [1,2,3,2,4] the function should return
[1,3,4] removing the element 2 because it appears more than once in the
original list (fig. 1(a)). The programmer describes the function specification
in a docstring (see fig.1(b), extracted from the benchmark). However, the
natural language specification is ambiguous; it can be interpreted in multiple
ways as it does not indicate if all copies of the duplicated elements should
be removed, or if one copy should be retained in the returned list. In this
case, the programmer intends the former, however, it is not uncommon to expect
that the program should fulfill the latter.

(a) Programmer intent for a function that removes from a list all instances of
numbers that have duplicates.

(b) Ambiguous natural language specification: it does not specify if all
copies or all but one copy of duplicated element should be removed. In this
case, the programmer intends the former.

⬇

1 def remove_duplicates(numbers: List[int]):

2 """ From a list of integers, remove all elements that occur more than once.
Keep order of elements left the same as in the input """

(c) Postconditions generated by GPT-4. Note that while both could be correct with a literal reading of the ambiguous natural language specification, only the second one is correct with respect to the actual developer intent ⬇ 1 assert len(set(numbers)) == len(set(return_list)) | ✗
---|---
⬇ 1 assert all(numbers.count(i) == 1 for i in return_list) | ✓

Figure 1.  An example of how postconditions or other formal specifications of
program behavior could be used to clarify ambiguous natural language
specifications.

(a) Original function plus java doc.

⬇

1 /** @return a new line with reversed direction.*/

2 public Line revert() {

3 final Line reverted = new Line(zero, zero.subtract(direction));

4 return reverted; }

(b) Bug report (not seen by the LLM)

Line.revert() only maintains $\sim$10 digits for the direction. This becomes
an issue when the line’s position is evaluated far from the origin.

(c) Two bug-catching post conditions generated by GPT 4

⬇

1 // Correct bug-finding postcondition 1

2 assert this.direction.negate().equals(returnValue.direction);

3 //Correct bug-finding postcondition 2

4 assert this.direction.dotProduct(returnVal.direction) == -1 *
this.direction.getNormSq();

Figure 2.  Example of how postconditions or other formal specifications of
program behavior could catch bugs. This example is a historical bug from
Defects4J (Math-9): the Line constructor does not return a new line with
enough precision. The postconditions were generated by GPT-4 in our
evaluation, and both catch the bug.

Figure 1(c) contains two postconditions, each satisfying one of the two
possible intents of the ambiguous docstring. The programmer writing the
remove_duplicates function can verify that the second postcondition “assert
all(numbers.count(i)==1 for i in return_list” correctly matches their intent,
by ensuring that all numbers that appear in the returned list occur exactly
once in the input list. On the other hand, the first postcondition incorrectly
asserts that the return value _return_list_ is a set representation of the
input list _numbers_. In this example extracted from the HumanEval benchmark,
it is not immediately clear at first glance what the user intent is.
Generating such postconditions from natural language allows for checkable and
unambiguous statements about a program’s intended behavior, formalizing a
user’s intent about a program.

####  1.1.2. Detecting Real-World Functional Bugs

In practice, postconditions generated in the target programming language can
be used in assertions, as demonstrated in fig. 1(c), to check the correctness
of a function, enabling the early detection of bugs or violations of a
programmer’s intent.

The example in Figure 2 shows how formal specifications can be used to catch
bugs in real-world programs. A bug from the Apache Commons Math project, the
function revert() calls a constructor Line() that should return a new Line
object with a reversed direction. The bug report
111https://issues.apache.org/jira//browse/MATH-938 associated with the issue
explains that revert() does not maintain enough precision, and fails in
certain scenarios. Both of the provided postconditions in Figure 2(c) catch
the bug by leveraging project-specific context and general mathematical
knowledge about the specifications of a reversed line.

###  1.2. Overview

In both of the illustrated examples, we demonstrated the use of GPT-4 to
generate postconditions from natural language specifications. While these
examples show that GPT-4 is able to generate postconditions that closely
capture informal intent and also detect bugs in program behavior, it is
unclear to what extent LLMs are capable of the LLM4nl2post problem in general.
In this paper, we pose the high-level question:

> Given a natural language description of a method and a candidate
> postcondition, how do we judge the quality of the postcondition?

We attempt to study this question through two high-level research questions:

  * •

RQ1: How well do LLM-generated postconditions formalize informal natural
language intent?

  * •

RQ2: Can LLM-generated postconditions help catch real-world bugs?

To answer these questions, we contribute by defining automated metrics for
measuring the usefulness of LLM-generated postconditions, describing different
ways to encode the problem statements to the input of an LLM, exploring
different LLMs, and performing an empirical investigation (both quantitative
and qualitative) on benchmarks across multiple programming languages. We start
by defining automated evaluation metrics for the correctness and completeness
(i.e., the discriminative power) of a postcondition (Section 2.1), and
proposing a generic “prompt” and variants to transform LLM4nl2post into an
input for LLM (Section 2.2). We evaluate RQ1 using a Python programming
dataset and present a detailed quantitative and qualitative analysis of the
quality of generated postconditions across different LLMs and prompt variants
(Section 3). Next, we evaluate RQ2 on a benchmark of real-world Java defects
and report on the quality of generated postconditions and their ability to
find bugs by distinguishing the fixed version from the buggy version (Section
4). Finally, we articulate the limitations (Section 6), discuss related works
(Section 5) and conclude.

###  1.3. Contributions

  * •

Evaluating the feasibility of LLMs to facilitate LLM4nl2post via an empirical
evaluation of the quality and usefulness of LLM generated postconditions on
multiple benchmarks in multiple mainstream programming languages.

  * •

A set of metrics (both correctness and completeness) for evaluating natural
language generated postconditions, validated through an empirical and
qualitative investigation. In particular, we believe this paper is the first
to propose the use of LLMs to derive a natural distribution of code mutants to
evaluate the completeness of specifications.

  * •

The finding that with sufficiently robust natural language descriptions, LLMs
can use LLM4nl2post to generate correct postconditions with high
discriminative power. We illustrate that with GPT-4 we can generate correct
postconditions for up to 96% of problems for our benchmark, EvalPlus, with
correct postconditions able to discriminate up to 81% of buggy programs on
average.

  * •

The findings that LLM-generated LLM4nl2post postconditions are precise enough
to capture real-world bugs in large industrial projects; LLM4nl2post
postconditions detect 70 historical bugs from industrial-scale Java projects.

##  2\. LLM4nl2post: Overall Approach

###  2.1. Problem formulation and metrics

In the following two subsections, we formalize the LLM4nl2post problem through
metrics to evaluate the quality of generated postconditions. Consider an
example $\langle{\it nl},{\it r},{\it T}\rangle$, where ${\it nl}$ is the
natural language description of a problem, ${\it r}$ is a reference code
implementation, and ${\it T}$ is a set of test inputs. For this section, we
assume that each test $i\in{\it T}$ is an input that assigns a value to the
input parameters and globals of ${\it r}$. We further assume that the
reference solution is deterministic and returns a single output value ${\it
ret}$ containing the output. In this simple setting, it suffices to only have
the set of inputs in ${\it T}$, as the desired output for each input $i$ can
be obtained by executing ${\it r}(i)$. For the purpose of postcondition
generation through an LLM, the set of tests ${\it T}$ is hidden from the LLM
that generates a postcondition. The reference implementation ${\it r}$ may or
may not be present during the postcondition generation. However, both ${\it
r}$ and ${\it T}$ are used to define the metrics for the offline evaluation
for a benchmark set.

####  2.1.1. Test-set correctness

Given an example $e\doteq\langle{\it nl},{\it r},{\it T}\rangle$, a candidate
postcondition ${\it post}$ is an assertion over the input and output states of
${\it r}$. For an expression $\it expr$ and a state $s$ that assigns valuation
to variables, let $\it eval(\it expr,s)$ be the result of evaluating $\it
expr$ after replacing the variables in $\it expr$ with their values from $s$.
A postcondition is correct if the reference implementation ${\it r}$ satisfies
it for every possible (legal) input. Therefore, a candidate postcondition
${\it post}$ is correct if for every input $i$, if ${\it r}(i)$ is the output
value, then $\it eval({\it post},(i,{\it r}(i)))$ is true, where $(i,{\it
r}(i))$ is the joint state of the input parameters and output return variable.
However, such a notion of correctness is difficult to establish in the absence
of formal verification tools, and may further require manual effort to
establish such proof even for verification-aware languages (Leino, 2010; Swamy
et al., 2011). We take a pragmatic approach, assuming that the test cases in
${\it T}$ are sufficiently comprehensive to approximate the space of all legal
inputs. Therefore, an expression ${\it post}$ is test-set-correct w.r.t. ${\it
T}{}$ (denoted as $\it correct_{{\it T}}$) iff $\forall i\in{\it T}:\it
eval({\it post},(i,{\it r}(i))==\it true$. Henceforth, we may refer to ”test-
set-correct” as simply correct, since correctness in the remainder of the
paper is with respect to the provided tests.

Given a set of $m$ postconditions from an LLM, we define a metric $\it
accept@{k}$ for $1\leq k\leq m$ to capture the statistical expected value of
containing at least one test-set-correct postcondition while sampling subsets
of size $k$ from the set of $m$ conditions. This is inspired by the $\it
pass@{k}$ metric proposed for evaluating the quality of correctness of
generated code given a set of tests (Chen et al., 2021).

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

(Test-set) correctness is a necessary condition for a valid and useful
postcondition, however, it is not sufficient. For example, the expression $\it
true$ vacuously satisfies any implementation $r$ for any input $i\in{\it T}$,
and is therefore correct. The value of a postcondition comes from how well it
captures the desired intent expressed in the natural language intent ${\it
nl}$. However, given that ${\it nl}$ is informal, we cannot establish a check
to ensure the association. Instead, we leverage the reference implementation
and tests as the source of ground truth for what the user intends. However,
this again poses the problem that the most desired postcondition is simply the
strongest postcondition of ${\it r}$ program, which is computationally
intractable (Dijkstra and Scholten, 1990). Instead, we use a concept of
completeness that measures the degree to which the postcondition distinguishes
the reference implementation ${\it r}$ from other incorrect implementations.

Inspired by mutation-testing literature (c.f. Jia and Harman (2010)) that
assigns a mutation score to a test $t$ based on the fraction of code mutants
“killed” or distinguished under $t$, we assign a measure of bug-completeness
to a postcondition ${\it post}$ as the fraction of code mutants that can be
distinguished given the set of tests ${\it T}$. Unlike traditional mutation
testing, we parameterize completeness with a semantically distinct code mutant
set $\it CM$ that are guaranteed to differ from ${\it r}$ (and from each
other) on at least one test in ${\it T}$. In other words, for each $c\in\it
CM$, there exists a test input $i\in{\it T}$ that distinguishes from ${\it r}$
(i.e., ${\it r}(i)\neq c(i)$) and (a possibly different) $i$ that
distinguishes from any other $c^{\prime}\in\it CM\setminus\\{c\\}$ (i.e.,
$c(i)\neq c^{\prime}(i))$. Given an example $e\doteq\langle{\it nl},{\it
r},{\it T}\rangle$, a $\it correct_{{\it T}}$ postcondition ${\it post}$ and a
set of distinct code mutants $\it CM$, we define the bug-completeness-score of
${\it post}$ as:

$\textit{bug-completeness-score}({\it post},\it CM,{\it T})\doteq|\\{c\in\it
CM\ |\ \exists i\in{\it T}:\it eval(post,(i,c(i)))==\it false\\}|/|\it CM|$

In other words, bug-completeness-score measures the fraction of code mutants
that fail the correct postcondition. If the bug-completeness-score of a
postcondition is 1, we say that the postcondition is bug-complete. One can
easily lift the idea to the completeness of a set postconditions ${\it P}$ by
taking a union of all the code mutants ”killed” using all the correct
postconditions in the set:

$\textit{bug-completeness-score}({\it P},\it CM,{\it T})\doteq|\bigcup_{{\it
post}\in{\it P}}\\{c\in\it CM\ |\ \exists i\in{\it T}:\it
eval(post,(i,c(i)))==\it false\\}|/|\it CM|$

Now, we discuss why we use a parameterized set of code mutants instead of
creating variants of ${\it r}$ by mutating different operators. We believe
that such a fixed set of mutation operators does not approximate real-world
bugs for two reasons: (a) first, since code mutants only differ from the
reference implementation in one or two operators at a time, it may not cover
mutations that are further away in the edit distance, and (b) it may not cover
subtle bugs that a human would write using different syntactic constructs
(e.g., a while loop instead of a for loop) or APIs. We propose the use of LLMs
to sample mutants from the natural distribution of implementations to the
problem described by the natural language intent ${\it nl}$. In other words,
we enumerate a set of likely implementations $\it Impls$ for ${\it nl}$ using
a LLM (such as GPT-4), and define $\it CM$ to be the subset of $\it Impls$
that differ from ${\it r}$ on at least one test $i\in{\it T}$, and also
pairwise distinct in terms of the tests in ${\it T}$.

###  2.2. Prompt Design for LLM-based Postcondition Generation

You have the following code context, function stub and natural language
specification (in the form of a code comment) for [FUNCTION NAME]. When
implemented, the function should comply with this natural language
specification: [PROGRAM CONTEXT, FUNCTION STUB, AND DOCSTRING HERE] Write a
symbolic postcondition for [FUNCTION NAME] consisting of exactly one assert
statement. For variables, use only the function input parameters and a
hypothetical return value, which we’ll assume is stored in a variable
return_val. If the postcondition calls any functions external to the program
context, they should only be those from the functional subset of [PROGRAMMING
LANGUAGE]. By this, we mean functions that are pure (i.e., no side effects)
such as [PROGRAMMING LANGUAGE-SPECIFIC EXAMPLE].

Although the postcondition should be less complex than the function itself, it
should not be trivial. It should encapsulate an aspect of the function without
implementing the function. The format of your response should be:
``` CODE FOR EXACTLY ONE POSTCONDITION WITH ASSERT HERE ``` Figure 3. Prompt
template for generating postconditions from natural language via chat models.
[Green] text was replaced with text specific to the programming language or
benchmark problem. Bolded text was included only in our simple prompt for
producing simpler postconditions. Underlined text was removed when we included
a reference solution in the prompt. We found that the italicized text greatly
improved the quality of the postconditions: without it, the model tended to
return point-based tests or code blocks with side effects.

We now describe how we leverage LLMs to generate high-quality postconditions.
Our goal is to produce expressions that are syntactically and semantically
valid while being as programming language agnostic as possible. We would also
like our postconditions to be symbolic (e.g., not point-wise tests), directly
executable, and side-effect free.

We design a few ”prompts” (textual inputs to the LLMs) based on a problem
description ${\it nl},$ and reference solution ${\it r}$. We design our
prompts for chat-based models. Several prompt iterations were considered until
all authors were satisfied by the output on a subset of example problems.
Figure 3 contains our postcondition generation prompts. As we describe below,
our prompt variations have 2 orthogonal axes (a) whether the reference ${\it
r}$ is included, and (b) requested postcondition complexity.

Our default prompt includes only the ${\it nl}$, not the reference code ${\it
r}$. This is useful for specification-driven AI-based programming scenarios
(Lahiri et al., 2022) where the user first accepts a few specifications that
are used to constrain (and prune) the code suggestions that AI generates. In
addition, we also provide a prompt that includes the reference code ${\it r}$
along with ${\it nl}$. This allows us to assess if natural language alone can
be as effective as code in conveying programming intent to an LLM.

On the other axis, we also consider a “simple” variation of the prompt that
explicitly instructs the LLM to generate postconditions that capture an aspect
of a function, rather than the whole function. We include this variation as we
noticed that LLMs have a tendency to construct a postcondition that is a fully
functional implementation of the problem. While useful, this has two pitfalls:
(a) the likelihood of a single complex postcondition being correct is lower,
and (b) users may have a difficult time understanding a complex (albeit
correct) specification.

We combine these two prompt variations into four distinct prompts in our
evaluation:

  1. (1)

Base prompt with only natural language description ${\it nl}$ (no reference
solution ${\it r}$)

  2. (2)

Base prompt with both reference ${\it r}$ and natural language description
${\it nl}$

  3. (3)

Simple prompt with only natural language description ${\it nl}$ (no reference
solution ${\it r}$)

  4. (4)

Simple prompt with both the reference ${\it r}$ and natural language
description ${\it nl}$

##  3\. RQ1: How well do LLM-generated postconditions formalize informal
natural language intent?

To assess if LLMs can generate high-quality postconditions that capture and
formalize intent, we report a detailed empirical study of LLM-generated
postconditions on a popular benchmark.

###  3.1. RQ1 Experimental Setup

####  3.1.1. Evaluation Benchmark

We use the benchmark EvalPlus, which consists of 164 Python programming
problems, each with an associated function stub and natural language
description in the form of a Python docstring along with a reference
implementation and validation tests (Liu et al., 2023). EvalPlus is a recent
update to the popular HumanEval benchmark (Chen et al., 2021), containing the
same programming problems but with the addition of a much more extensive test
suite containing an average of 775 tests per problem. We choose EvalPlus as
our target dataset because each example has (a) a descriptive natural language
intent, (b) a set of extensive test inputs, and (c) a unique reference
solution. Using all three of these components we can evaluate if a
postcondition formalizes the user intent expressed in the natural langauge
docstring ${\it nl}$ (a) while satisfying the reference solution.

####  3.1.2. Large Language Models

We generate postconditions using three recent chat-based models, representing
a mix of closed and open-source approaches, that have demonstrated state-of-
the-art performance on various programming tasks:

  * •

_OpenAI: GPT-3.5 and GPT-4_ are based on the pre-trained GPT-3 model, which is
further finetuned using Reinforcement Learning with Human Feedback (RLHF)
(Ouyang et al., 2022). While GPT-3.5 and GPT-4 are not explicitly fine-tuned
for code generation tasks, they have demonstrated strong capabilities on a
variety of code generation tasks (Olausson et al., 2023; Fakhoury et al.,
2023). We access the model using OpenAI APIs for the gpt-3.5-turbo and gpt-4
endpoints.

  * •

_The BigCode Project: StarChat._ StarCoder (Li et al., 2023) is an open-access
16B parameter model pre-trained on The Stack (Kocetkov et al., 2022), one
trillion tokens sourced from 80+ programming languages, GitHub issues, Git
commits, and Jupyter notebook. In this paper, we use _StarChat_ 222HuggingFace
model identifier HuggingFaceH4/starchat-alpha, a version of StarCoder fine-
tuned for assisting coding. StarChat is currently one of the few open-access
chat model alternatives to GPT-3.5 and GPT-4, permitting replication of and
comparison with our results. Using this model allows us to use the same prompt
we used for the OpenAI models, rendering a fairer comparison.

####  3.1.3. Postcondition Generation

For each problem in EvalPlus, we generate 10 postconditions for each the 4
prompt variants (Section 2.2) per LLM model. All postconditions are generated
using a temperature of 0.7. We use 0.7 as it is the default temperature for
both GPT-3.5 and GPT-4 models, and has been found to be a reasonable
temperature for code generation tasks333We also considered additional
temperatures of 0.2 and 1.2. However, since high-level trends were the same
regardless of temperature, we only report results of 0.7 here for clarity. As
we consider four prompt variants, in total we generate 40 postconditions per
problem per model. This results in 19,680 postconditions across all variants,
models, and EvalPlus problems.

####  3.1.4. Code Mutant Generation

To generate the set of code mutants $\it CM$ needed for bug-completeness, we
use an LLM (GPT-3.5 with temperature 0.9) to generate a set of codes that
satisfy the natural language intent ${\it nl}$, and filter the ones that fail
at least one test in ${\it T}$. We generate 200 code solutions to each problem
and then save only those that fail the test suite. We term these bugs as
natural code mutants, as they represent natural yet buggy implementations for
the problem description. However, we noticed that for some examples, the
number of such natural code mutants is fairly small. To amplify the set of
buggy codes, we generate 200 additional buggy codes by explicitly instructing
GPT-3.5 to include an error in its solution. As mentioned in Section 2.1.2, we
only retain distinct buggy codes so that no two mutants fail the same set of
tests. The number of unique buggy codes varies per problem, ranging from 4 to
233 with a median of 55. While we combine the two bug sources, we also
consider the natural mutants alone in our evaluation to see if the source of
the bug impacts the efficacy of our metrics.

###  3.2. RQ1-Results: Do LLM-generated postconditions formalize user intent?

We now discuss the results of our empirical and qualitative evaluations,
structured around postcondition correctness, postcondition completeness, and
qualitative insights.

####  3.2.1. Postcondition Correctness

Model | Prompt |  Prompt has: NL Only=✗ ref code=✓ |  | Accept
---
@ 1
| Accept
---
@ 5
| Accept
---
@ 10
| x/164
---
correct
GPT-3.5 | Base | ✗ | 0.46 | 0.80 | 0.87 | 143
GPT-3.5 | Base | ✓ | 0.49 | 0.81 | 0.88 | 145
GPT-3.5 | Simple | ✗ | 0.55 | 0.82 | 0.87 | 143
GPT-3.5 | Simple | ✓ | 0.56 | 0.82 | 0.88 | 144
GPT-4 | Base | ✗ | 0.63 | 0.83 | 0.88 | 144
GPT-4 | Base | ✓ | 0.71 | 0.89 | 0.91 | 150
GPT-4 | Simple | ✗ | 0.77 | 0.94 | 0.96 | 158
GPT-4 | Simple | ✓ | 0.76 | 0.92 | 0.96 | 157
StarChat | Base | ✗ | 0.21 | 0.61 | 0.82 | 134
StarChat | Base | ✓ | 0.20 | 0.59 | 0.77 | 126
StarChat | Simple | ✗ | 0.25 | 0.69 | 0.85 | 139
StarChat | Simple | ✓ | 0.23 | 0.67 | 0.86 | 141
Table 1.  Test-set correctness on EvalPlus for three models (GPT-3.5, GPT-4,
and StarChat), differing prompt complexities (base vs. simple), and including
or omitting the reference solution in the prompt. Darker highlighted cells are
more correct. Bolded values are the largest for a specific model.

Table 1 has our test-set-correctness (Section 2.1.1) results. Overall, we find
that for EvalPlus, LLM-generated postconditions are likely to be test-set
correct; in our best-performing prompt variation, 77% of postconditions were
correct and a correct postcondition was generated for 96% of problems
(158/164). As we show later in this section, test-set correctness on EvalPlus
largely corresponds to true correctness. Our correctness results indicate that
LLMs have the potential to reliably generate correct postconditions from
natural language specifications.

Regardless of the prompt variation, GPT-4 postconditions were the most likely
to be correct ($0.63\leq$ accept@1 $\leq 0.77$) followed by GPT-3.5
($0.46\leq$ accept@1 $\leq 0.56$). StarChat postconditions were consistently
the least correct, with accept@1 between 0.21 and 0.25. While the raw number
of correct StarChat postconditions was low, the number of benchmark problems
with at least one correct postcondition was relatively high, ranging from 78%
to 86% depending on the prompt.

As described in section 2.2, we consider both a base postcondition prompt and
a simple prompt for generating simpler postconditions that capture only an
aspect of program behavior. Regardless of LLM model, simple postconditions are
more likely to be correct than base postconditions. Using a paired students
$t$-test (Hsu and Lachenbruch, 2014) between accept@1 ablation pairs where the
only difference is the prompt complexity type, simple prompt postconditions
are significantly more likely to be correct with $p=0.008$, a large effect
(standardized Cohen’s $d=1.73$). This indicates that when prioritizing
correctness, using a prompt that explicitly asks for simpler postconditions
improves the result.

We also compared the efficacy of generating postconditions from natural
language alone to generating when a reference solution is included in the
prompt. We did not observe a significant difference in accept@1 between
postconditions generated with natural language specifications alone and those
including a reference solution ($p=0.42$). This indicates that the presence of
a reference solution does not necessarily enhance postcondition correctness
when compared to natural language alone. Therefore, it might be feasible to
rely solely on natural language intent (when comprehensive enough) without
needing to provide a reference solution.

Correctness false positives. While EvalPlus has more comprehensive tests than
its predecessor HumanEval, it is still possible that the tests do not
perfectly discriminate between all correct and incorrect codes. If so, our
test-set correctness metric may have false positives: postconditions we mark
as correct but do not accurately capture the natural language intent. In our
qualitative analysis (see Section 3.2.3), we validate our metric for EvalPlus:
we find only one problem (# 122) with false positives. Overall, this rate is
fairly low. To see this, we also compare our results to the hypothetical
results if using HumanEval (the predecessor to EvalPlus that contains the same
problems with many fewer tests). The HumanEval results contain 7% false
positives for accept@10 for GPT-4, much higher than our results. Thus, we find
that our test-set correctness is a reasonable approximation for true
correctness on EvalPlus (but not on HumanEval due to a less comprehensive set
of tests).

RQ1 Summary: Postcondition Correctness On EvalPlus, LLMs are good at producing
correct postconditions from informal natural language specifications. All
prompt variants generate a correct postcondition for at least 77% and up to
96% of problems. GPT-4 consistently outperformed the GPT-3.5 and StarChat.
Explicitly asking for simpler postconditions leads to more correct
postconditions via LLM4nl2post. However, we do not observe a significant
difference between including or omitting a reference solution in the prompt;
using natural language (when descriptive) alone can be just as powerful.

####  3.2.2. Postcondition Completeness

While our test-set correctness results are encouraging, test-set correctness
is necessary but not sufficient for assessing if a postcondition meaningfully
captures the natural language specification. To capture a notion of
completeness, we measure bug-completeness for all test-set correct
postconditions (see Section 2.1). Table 2 contains our results. We report both
the percentage of postconditions that are bug-complete (kill all unique code
mutants) and the average bug-completeness score (fraction of code mutants
killed). The results indicate the GPT-4 generated postconditions can kill all
the code mutants for up to $61.6\%$ (and up to $62.2\%$ when combining
postcondtions) of examples in EvalPlus. Overall, both GPT-3.5 and GPT-4
generate relatively bug-complete postconditions, with average scores of up to
0.76 and 0.85 respectively. That is, the average correct postcondition
generated by these models can discriminate over three-quarters of unique buggy
code mutants. The bug-completeness scores for StarChat were lower but still
substantial, catching up to one-third of mutants. Our bug-completeness results
suggest that LLMs, especially the advanced models like GPT-3.5 and GPT-4, can
use natural language to produce postconditions that meaningfully capture
desired aspects of program behavior.

.  Prompt has: NL Only=✗ ref code=✓ % problems with bug- complete % problems
union bug- complete Avg bug-completeness-score for correct postconditions
Model Prompt % bug- complete Natural bugs All bugs GPT-3.5 Base ✗ 15.4 42.1
48.2 0.62 0.72 GPT-3.5 Base ✓ 18.5 47.0 49.4 0.70 0.76 GPT-3.5 Simple ✗ 8.1
29.3 33.5 0.44 0.55 GPT-3.5 Simple ✓ 14.0 37.2 41.5 0.58 0.62 GPT-4 Base ✗
35.1 61.6 62.2 0.81 0.85 GPT-4 Base ✓ 34.9 58.0 61.6 0.78 0.82 GPT-4 Simple ✗
9.2 26.2 29.3 0.40 0.52 GPT-4 Simple ✓ 8.9 29.3 36.0 0.47 0.56 StarChat Base ✗
0.8 7.3 8.5 0.13 0.24 StarChat Base ✓ 1.4 9.1 11.0 0.23 0.30 StarChat Simple ✗
1.5 6.7 7.3 0.16 0.24 StarChat Simple ✓ 3.0 17.1 17.7 0.23 0.36

Table 2. Table of bug-completeness for EvalPlus. % bug-complete is the % of
postconditions that detect all buggy code mutants. % problems with bug-
complete is the % of all EvalPlus problems with at least one bug-complete
postcondition. % problems union bug-complete is the % of problems where the
union of correct postconditions is bug-complete. Finally, the last two columns
are the average bug-completeness-score, a fraction between 0 and 1, for all
correct postconditions, normalized by EvalPlus problem. We report this for
both natural and all generated code mutants. Bolded values are the largest
value per column per model.

In contrast to the correctness results in Section 3.2.1, base prompt
postconditions generally have higher bug-completeness scores than simple
prompt postconditions (up to a 30% difference). While the difference is not
quite significant (paired $t$-test $p=0.06$), this trend hints that the simple
prompt may generate more complex postconditions at the expense of bug-catching
power. Even so, simple postconditions still meaningfully capture aspects of
program behavior: simple GPT-4 and GPT-3.5 postconditions discriminate over
half of unique buggy mutants.

We also compare the bug-completeness of postconditions generated from natural
language intent alone to those generated with a reference solution in the
prompt. While the difference was not quite significant, the average bug-
completeness score was 5% higher for the case with the reference code included
($p=0.06$). From our qualitative investigation, this seems to be caused by an
increase in the number of postconditions that are functional re-
implementations of the reference solution.

Natural vs. Artificial bugs. To help validate our proposed bug-completeness
metric (see Section 2.1), we examine the impact of using natural or artificial
LLM code generation bugs. As shown in Table 2, our completeness metric was
consistently (though not always substantially) lower when only considering
natural bugs; naturally occurring LLM code generation bugs are harder to kill
via LLM4nl2post than artificially seeded bugs. This finding highlights a
potential limitation in using artificially seeded faults to assess
postcondition correctness as it may artificially inflate the metric. However,
generating unique natural bugs is more expensive than using artificial bugs.
To ensure metric robustness, augmenting the evaluation metric with artificial
bugs may still be useful.

RQ1 summary: Postcondition Completeness We find that for the benchmark
EvalPlus, LLM4nl2post postconditions generated by GPT-3.5 and GPT-4 can
meaningfully capture program intent especially when using our base prompt: the
average correct postcondition generated by these models can discriminate
three-quarters of unique buggy code mutants depending on the prompt variation.

####  3.2.3. LLM4nl2post Postcondition Quality: A Taxonomy

To construct a taxonomy of the types of postconditions generated by LLMs, we
perform a structured qualitative analysis on a significant sample of
postconditions, generated using the best-performing prompt version: GPT-4 with
the simple prompt and no reference solution in the prompt. To construct the
taxonomy we first select a sample of candidate problems from EvalPlus and
their associated set of generated postconditions, consisting of 230
postconditions from 23 problems. The first two authors developed and agreed
upon a set of qualitative coding categories such as completeness, partial
correctness, and postcondition structure. They then coded all 230
postconditions, ultimately generating a taxonomy of LLM4nl2post
postconditions. The first author then used the taxonomy to code an additional
670 postconditions for a total of 900 coded postconditions from 139 problems
in the EvalPlus benchmark. We present this taxonomy in Table 3 and connect the
categories to postcondition correctness and completeness.

Table 3.  Our taxonomy of LLM4nl2post postconditions. Taxonomy elements are atomic postcondition structures that can be combined to create more complex postconditions. % test-set correct and bug-completeness columns are defined in Section 2.1. Example postconditions are in Python and adapted directly from our EvalPlus results, only modified for space. We verify our taxonomy categories with a separate analysis on a subset of Java postconditions in RQ2 (see section 4.2.3), giving confidence our taxonomy generalizes.) Category |  Example |  % of all post- conditions |  Avg bug-co- mpleteness nat. vs all
---|---|---|---
Type Check | assert isinstance(r_val, int) | 47.4 | 0.14 / 0.27
Format Check | assert r_val.startswith("ab") | 11.2 | 0.43 / 0.57
Arithmetic Bounds Check | assert r_val >= 0 | 30.8 | 0.23 / 0.34
Arithmetic Equality Check | assert r_val[0] == 2 * in_val | 17.5 | 0.82 / 0.89
Container Property | assert len(r_val) > len(in_val) | 27.0 | 0.45 / 0.57
Element Property | assert r_val[0] % 2 == 0 | 12.6 | 0.39 / 0.53
Multi-Element Check | assert all(ch.isalpha() for ch in r_val) | 8.3 | 0.23 / 0.44
Implication | assert (r_val == False) if ’A’ not in string | 12.7 | 0.58 / 0.64
Null Check | assert r_val is not None | 4.4 | 0.40 / 0.50
Average |  |  | 0.32 / 0.46

The first thing we noticed while classifying the LLM-generated postconditions
is that a single postcondition often consists of multiple atomic
postconditions, conjoined using && (logical and). For example, 33% of LLM-
generated postconditions that we analyzed contain multiple simpler
postconditions connected by &&. We categorize nine different basic types of
such atomic properties.

Table 3 has an example of each atomic postcondition type, along with its
dataset prevalence and average bug-completeness scores.

We did not observe a significant relation between postcondition type and
correctness. For bug-completeness, however, some atomic postcondition types
are more powerful than others. For example, postconditions coded as Type
Checkers only killed 27% of bugs on average while Implications and Arithmetic
Equality Checkers killed 64% and 89% of bugs respectively. This difference was
particularly pronounced for natural bugs (see Sections 2.1 and 3.1.4), where
Type Checkers only killed 14% of bugs on average. As postcondition type is
correlated with completeness but not with correctness, our taxonomy may have
implications for ranking or prioritizing postconditions

Additionally, the postcondition type completeness differences may partially
explain the lower postcondition completeness of StarChat postconditions
reported in section 3.2.2; while we do not perform a systematic qualitative
analysis of the StarChat data, we do observe that the majority of correct
StarChat postconditions are non-conjoined Type Checks, the weakest
postcondition type. In contrast, only 16% of postconditions generated by GPT-4
are non-conjoined Type Checks (the majority of Type Checks are in combination
with other atomic checks).

RQ1 summary: Taxonomy of Postcondtitions We qualitatively identify nine
possibly overlapping atomic categories of LLM-generated postconditions. While
we observe minimal differences in test-set correctness, bug completeness
varied significantly; the weakest postcondition type, Type Checks on average
killed only 14% of natural bugs while the strongest (Arithmetic Equality Check
killed 82% of natural bugs, a 6x difference.

##  4\. RQ2: Can LLM4nl2post help catch real world bugs?

Beyond understanding whether LLMs can capture natural language intent via
executable postconditions, we also want to understand LLM4nl2post’s real-world
potential. To do so, we investigate the second motivating use case in Section
1.1: finding bugs in an existing code base. We evaluate LLM4nl2post’s bug-
catching potential using Defects4J (Just et al., 2014), a benchmark of
historical Java bugs.

###  4.1. RQ2–Research Methodology and Experimental Setup

We outline our methodology for evaluating the capabilities of postconditions
to catch real-world bugs: we describe the target benchmark Defects4J, discuss
prompt variations for Java, and provide our criteria for bug-distinguishing
postconditions.

####  4.1.1. Benchmark: Defects4J

To evaluate the bug-catching capabilities of LLM-generated postcondtions we
use Defects4J 2.0 (Just et al., 2014), a well-known benchmark of 835 manually
curated real-world bugs and their fixes gathered from 17 Java projects. For
each bug, the existing dataset contains a set of bug-reproducing test cases
(trigger tests), and regression test cases which load the class in which the
method under test is contained. Each bug in Defects4J also contains a
PRE_FIX_REVISION and POST_FIX_REVISION version with the buggy/fixed versions
of the code respectively. We consider a postcondition to be test-set-correct
if it passes all trigger and regression tests on POST_FIX_REVISION.

As our postcondition prompt leverages functional syntax introduced in Java 8
(see the postcondition in figure 4(c) as an example), we only consider bugs
from Defects4J that are reproducible when compiled targeting Java 8. As a
result, we evaluate on subset of 525 total bugs. Each bug may involve changes
to multiple functions, for which we each generate postconditions. In total 840
functions are modified across the 525 bugs.

####  4.1.2. Bug Distinguishing Postconditions

To evaluate whether LLM-generated postconditions are capable of catching real-
world bugs, we instrument the PRE_FIX_REVISION and POST_FIX_REVISION versions
of a function with each associated postcondition. We consider a generated
postcondition to be _bug-distinguishing_ if it satisfies the following
criteria:

  1. (1)

The postcondition passes all the trigger and regression tests, on the
POST_FIX_REVISION of a function.

  2. (2)

The postcondition fails one of the trigger tests or regression tests on the
PRE_FIX_REVISION, i.e. the buggy version, of the function.

The Defects4J benchmark ensures that the difference between the
PRE_FIX_REVISION and POST_FIX _REVISION versions is minimized to only changes
related to the bug-fix. Therefore, assuming a comprehensive test suite, any
distinguishing postcondition satisfying the above criteria is related to the
(bug-related) change for the example.

Finally, similar to our qualitative evaluation for RQ1 (see Section 3.2.1) we
qualitatively analyze bug-discriminating postconditions to gain greater
insight and asses their quality.

####  4.1.3. Prompt Design and Ablations

To generate postcondtions for buggy functions in the dataset, we use the same
prompt as in RQ1 (see Figure 3). Designed as language agnostic, the only
change needed to adapt the prompt for Defects4J is including additional code
context. Given that Defects4J problems are extracted from real-world projects,
functions are comparatively more complex than those in EvalPlus and are often
tightly coupled with other project functions. Our initial investigations found
that without some file-level context, LLMs rarely generate meaningful
postconditions that also compile. Therefore, we include additional class and
type-related context in the prompt. Given the limited context window of the
LLMs used, we greedily include methods in the call graph for the buggy
function (ordered by in-file placement) until the prompt tokens are exhausted.
The call graph and in-file dependencies are determined using the Java language
binding for Tree-sitter444https://tree-sitter.github.io/tree-sitter/.

For each buggy function, we use a combination of function and class-level in-
file comments to formulate a natural language specification, with the most
common source being the modified function’s JavaDoc. We do not generate
additional natural language (i.e., through code summarization) nor do we use
text from external documentation or historical bug reports: all natural
language is pulled directly from the modified function’s source code file.

We choose to use the simple version of the prompt from RQ1, as we found that
this version led to more correct postconditions than did the base version.
Following the approach in RQ1, we report two variants of the prompt: 1) that
only include the natural language of the function to be specified and 2) that
include both the natural language and the code of the buggy function body:

  1. (1)

Simple prompt with natural language and code context (no buggy code)

  2. (2)

Simple prompt with natural language, code context, and buggy implementation

For each variant, we generate 10 postconditions for every function modified
between the buggy and fixed project versions (840 functions across 525 unique
bugs).

We choose to generate postconditions using two of the three earlier introduced
models, used in RQ1: GPT-4 and StarChat. Given that GPT-4 and GPT-3.5 are
comparable, closed-access chat models from OpenAI, we choose to focus on GPT-4
as it shows superior performance in RQ1. We choose to use StarChat as it is
one of the few open-source chat-based models available. In total, we evaluate
33,600 postconditions (2 models * 2 ablations * 10 postconditions * 840
functions).

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

We detail our findings on if LLM4nl2post postconditions are test-set correct,
and if they can catch bugs in real-world industrial-scale projects. We find
that even with the increased complexity over EvalPlus, GPT-4 is still able to
produce correct postconditions for Defects4J at a high rate. In addition, both
GPT-4 and StarChat are able to generate bug-discriminating postconditions for
a subset of Defects4J bugs. All bug-discriminating postconditions were further
analyzed via a qualitative analysis to gain insight into the ability of LLMs
to catch bugs via LLM4nl2post.

####  4.2.1. Test-set correctness

Model |  Prompt has: NL Only = ✗ buggy code = ✓ | Compiles | Test-set correct |  # disting- uishable bugs
---|---|---|---|---
@1 | @5 | @10 | @1 | @5 | @10
GPT-4 | ✗ | 0.65 | 0.86 | 0.89 | 0.32 | 0.57 | 0.66 | 35
GPT-4 | ✓ | 0.73 | 0.90 | 0.93 | 0.39 | 0.66 | 0.75 | 47
StarChat | ✗ | 0.25 | 0.68 | 0.83 | 0.11 | 0.38 | 0.55 | 19
StarChat | ✓ | 0.29 | 0.72 | 0.84 | 0.12 | 0.39 | 0.56 | 24
Table 4. Table containing our Defects4J results for postconditions generated
for 840 methods across 525 historical bugs. We report the likelihood of
generated postconditions to compile, and the likelihood that they pass all
tests when instrumenting the fixed function (test-set correct columns). _#
distinguishable bugs_ is the number of bugs for which at least one generated
postcondition was distinguishing (see Section 4.1.2).

Our full test-set correctness results for Defects4J are in table 4. We find
that while lower than the results from EvalPlus, GPT-4 still generate a
significant number of test-set correct postconditions with respect to the
fixed version of a function (e.g., correct with respect to programmer intent),
achieving accept@1 of up to 0.39 and accept@10 of up to 0.75. StarChat
performs worse, with accept@1 and accept@10 of 0.12 and 0.56 respectively. We
note that these numbers may be higher in practice if postconditions are
filtered by those that compile (see table 4, Compiles column). In general,
including the buggy code in the prompt leads to more test-set correct
postconditions. This contrasts with the results from EvalPlus, where we did
not observe a difference. We hypothesize that this is the case because of (a)
the comments not being completely descriptive, and (b) the increased program
and object complexity in Defects4J, as supported by the fact that
postconditions are also less likely to compile when the buggy code is omitted
from the prompt.

####  4.2.2. Bug-discriminating postconditions

We find that LLMs are able to generate postconditions that distinguish between
buggy and fixed code in real-world projects with respect to regression and
trigger tests. As seen in Table 4, GPT-4 was able to generate distinguishing
postconditions for up to 47/525 (9%) bugs in our evaluation. StarChat caught
fewer, but still generated postconditions that distinguished up to 25 bugs.
Across all prompt variants and models, we were able to generate a bug-
distinguishing postcondition for 70 unique bugs in Defects4J, 13.3% of all
bugs considered.

RQ2 summary: Correctness and bug catching power on Defects4J We find that
postconditions generated by LLMs from informal natural language specifications
are often test-set correct for real-world functions (accept@10 up to 0.75) and
can be powerful enough to catch real-world bugs (LLM4nl2post discriminates 70
bugs in Defects4J).

####  4.2.3. Qualitative analysis of bug-discriminating postconditions

We conduct a qualitative evaluation of the bug-distinguishing postconditions
to 1) determine if the earlier proposed taxonomy (Sec.3.2.3) generalized to
Java postconditions and 2) gain insight into how LLM4nl2post postconditions
discriminate real-world bugs. We observed additional evidence both motivating
the potential usefulness of LLM4nl2post and examples of why LLMs may be a good
tool to solve this problem. To communicate these findings, we detail two
cases.

(a) Buggy function stub and javadoc.

⬇

1 /** Render the text and return the rendered Options in a StringBuffer.

2 * @param width The number of characters to display per line

3 * @param nextTab The position on the next line for the first tab.

4 * @param text The text to be rendered.*/

5 StringBuffer renderWrappedText(StringBuffer sb, int width, int nextTab,
String text);

(b)  Bug report indicating that the function sometimes erroneously renders
text with more than width characters per line, behavior that directly
conflicts with the Javadoc.

The method... has couple of bugs in the way that it deals with the [nextTab]
variable. This causes it to format every line beyond the first line by
[nextTab] too many characters beyond the specified width.

(c) Bug catching post conditions generated by GPT-4. rVal is the function
return value. This postcondition was generated without the buggy function code
in the prompt.

⬇

1 // Checks if the rendered text does not exceed the specified width per line

2 assert rVal.toString().lines().allMatch(line -> line.length() <= width);

Figure 4.  Example from Defects4J (Cli project, bug 8) where the bug can be
caught via LLM4nl2post. In this case, there is a bug in the implementation for
calculating the width of lines when wrapping output text. The natural language
function description specifically says that each line must be at most width
characters long. GPT-4 translates this intent into the provided postcondition,
which correctly catches the bug.

The first case is a historical bug from the Apache Commons CLI
project.555Project page: https://commons.apache.org/proper/commons-cli/, Bug
report: https://issues.apache.org/jira/browse/CLI-151 As shown in figure 4,
the program should render multi-line text such that 1) white space padding is
added at the beginning of every line after the first one and 2) that no line
length exceeds a specified width. The requirement that each line should be
width characters long is clearly specified in the Javadoc. However, the
program sometimes incorrectly rendered lines longer than width due to a bug in
the white space padding implementation. In our evaluation, GPT-4 generated
multiple postconditions that catch this bug, including the example in 4(c).
These bug-catching postconditions were generated by both prompt variations.
This example evidences both that 1) informal natural language can meaningfully
telegraph code bugs and 2) modern LLMs, such as GPT-4, can sufficiently
formalize natural language intent to capture the disagreement. Overall, this
example shows the potential of LLM4nl2post to unearth coding inconsistencies
solely from informal natural language documentation.

For our second example, we refer back to one of our initial examples
motivating LLM4nl2post in Section 1.1, figure 2. This example was adapted from
Defects4J, and consists of a historical bug in another popular Apache library
project, Commons Math.666Project web page:
https://commons.apache.org/proper/commons-math/, Bug report:
https://issues.apache.org/jira/browse/MATH-938 In this bug, a method returning
a reversed instance of a mathematical Line object does not retain sufficient
precision in its internal state. GPT-4 is again able to generate multiple
postconditions that correctly detect this bug: both postconditions in figure 2
are actual postconditions from our evaluation. As with the first example, this
example demonstrates the potential of LLMs to generate postconditions powerful
enough to capture real-world bugs. However, this example additionally provides
evidence that LLMs in particular are helpful for realizing LLM4nl2post. Both
postconditions detect the bug by leveraging general mathematical knowledge
about the properties of a reversed line. The second postcondition in
particular exemplifies the ability of LLMs to dynamically combine methods such
as dotProduct from the project file’s context with algebraic world knowledge
that is external to the project’s code.

Finally, we used our qualitative analysis of the bug-discriminating
postconditions to see if our proposed LLM postcondition taxonomy (see table 3)
generalizes to Java. Overall, we found that it does. Annotating a subset of
100 bug-discriminating GPT-4 postconditions, we find that all 100 can be fully
categorized by our taxonomy. The main difference is that Defects4J
postconditions rely heavily on calling other class functions provided in the
program’s context: 39% of annotated postconditions call at least one such
function. However, this difference may have more to do with the complexity of
the benchmark than the difference in programming language. We also attempted
to establish the correctness of these postconditions, beyond just test-set
correctness. This may happen if the test suite is not comprehensive. We were
able to establish the correctness for 80% of the postconditions, and found
only 5% false positives. The need to understand project-specific invariants
precluded us from classifying the correctness of the remaining postconditions.

RQ2 summary: Features of bug-discriminating postconditions Bugs caught by
postconditions demonstrate both the potential usefulness of LLM4nl2post and
why LLMs may be a good tool to facilitate it. Additionally, our qualitative
results indicate that the postcondition taxonomy we generated for Python may
generalize to other mainstream languages including Java.

##  5\. Related Work

###  5.1. Specification Generation

A specification provides a comprehensive description of a program’s intended
behavior, encompassing the functional relationships between inputs and
outputs, as well as the internal state dynamics. Specifications may vary in
formality, ranging from informal descriptions such as API documentation to
formal representations like test cases or runtime assertions. The applications
of program specifications are extensive and include bug identification
(Jackson, 1992; Arcuri, 2008), verification (Chalin et al., 2006; Mike et al.,
2004), specification-driven development (Rutledge et al., 2014; Ostroff et
al., 2004; Leitner et al., 2007), code comprehension (Bowen et al., 1993), and
numerous others. Our goal is to generate formal and functional specifications
in the form of postconditions, articulating the desired input-output
relationship of a code, given the informal natural language description. There
has been a long line of work for automatically inferring specifications using
static analysis (Shoham et al., 2007), abstract interpretation (Cousot et al.,
2012), dynamic analysis (Ernst et al., 1999), and so on. While most of these
existing works rely on a code implementation inferring the specification of
existing code, our approach is to infer the desired behavior of the code from
natural language. Similar to us, several approaches attempted to generate
specification by analyzing API documentation or code comments using different
natural language processing techniques such as named pattern matching (Tan et
al., 2012; Pandita et al., 2012; Tan et al., 2007, 2011), text normalization
(Blasi et al., 2018), entity recognition (Zhong et al., 2009), natural
language parsing (Zhou et al., 2017), etc. Being dependent on mostly hand-
crafted rules and heuristics, most of these techniques only work on the semi-
structured natural language format of the input and are not easily extensible
across different programming languages and domains. In contrast, our technique
relies on LLMs for world knowledge and our experiment shows the extensibility
of our technique in two different languages – Python and Java.

###  5.2. Machine Learning for Specifications

Machine Learning based approaches for specification generation have shown
promise in several orthogonal directions, including synthesizing test oracles
(Tufano et al., 2022; Mastropaolo et al., 2022; Dinella et al., 2022),
improving test coverage (Lemieux et al., 2023), generating unit tests (Tufano
et al., 2020; Lahiri et al., 2022) and so on. Depending on the application
scenario, the specifications generated by these approaches are dependent on
different inputs. For instance, TOGA (Dinella et al., 2022) generates the test
oracle for a given test prefix without relying on a method implementation.
AthenaTest (Tufano et al., 2020), on the other hand, generates both the input
and the oracle of a unit test from the implementation of the focal method.
Closer to our work, TiCoder (Lahiri et al., 2022) leverages LLM to generate
test input and output to formalize the user intent. While these approaches
focus on generating concrete test cases (and potentially oracles), our
approach is geared toward generating abstract functional relationships between
the input and output of a procedure, which allows us to reason about a range
of inputs. Similar to our work, EvoSpex (Molina et al., 2021) generates
functional relationships of input-output with evolutionary learning. While
their approach is aimed at summarizing existing program behavior (and
therefore cannot be used to find bugs), our approach contributes towards
generating formal specifications of desired input-output behavior. Recent work
by Vikram et al. (2023) proposes to leverage LLM for generating property-based
tests (PBTs). Speculyzer (Key et al., 2022) uses LLMs to enumerate likely
properties and inputs similar to PBT, but use them as heuristics to improve
code generation. Unlike our work, they do not seek to evaluate the correctness
and completeness of these specifications. In addition to the input-output
specification generation, machine learning has been applied to generate
intermediate specifications of a code such as invariants, using traditional
machine learning (Garg et al., 2016; Sharma and Aiken, 2016), deep learning
(Yao et al., 2020; Ryan et al., 2020), and LLMs (Pei et al., 2023).

##  6\. Limitations and Threats to Validity

##### Data leakage.

One potential concern to the generalizability of the study is the use of
popular benchmarks EvalPlus and Defects4J which are included in The Stack
(Kocetkov et al., 2022), the dataset used to train StarChat, and may have been
included as part of training datasets for both GPT-3.5 and GPT-4. The risk of
data leakage could pose a threat to the internal validity of our study.
Nevertheless, this concern is partially mitigated by the target task: the use
of models to produce postconditions, which are not artifacts of either
dataset. To our knowledge, postconditions have not been previously generated
as part of any public-facing dataset.

_Stability of models’ output._ Two of the models used in the experiments are
accessed using OpenAI web APIs. OpenAI models are not open-access and are
often updated or deprecated. This poses a threat to the replicability of our
study. To mitigate this threat, we plan to make available all postconditions
generated by the closed-access models. We also use the open-access StarChat,
and will share the generated artifacts. In addition, we report results using
_accept@k_ , similar to the widely adopted metric _pass@k_ (Chen et al.,
2021), which accounts for the stochasticity of model output.

_Measure of postcondition completeness._ Our metric for postcondition
completeness relies on a set of generated code mutants. The code mutants are
generated to cover the space of possible bugs in the target function, however,
the set of code mutants generated per problem will never represent a
comprehensive set of possible bugs. Therefore, our measure of completeness is
dependent on the range and quality of bugs covered in the set of mutants. This
poses a threat to the internal validity of our study. To mitigate this threat
we maximize the diversity of bugs by retaining only distinct mutants, and
generate up to 233 buggy codes per problem.

_Generalization of findings._ Given the relatively small number of bugs (525)
considered in the Defects4J benchmark, our findings may not generalize to
arbitrary bugs across different languages and repositories. We partially
mitigate this threat by using real-world bugs from open-source projects and
evaluating the capabilities of LLMs on both Python and Java benchmarks. In
addition, the proposed taxonomy of postconditions (Section 3.2.3) is
representative of only the programs in the EvalPlus benchmark and may not
generalize across languages or program complexities.

##  7\. Conclusion

Natural language descriptions of program intent are abundant in software, but
they are rarely leveraged in practice due to their inherent ambiguity and the
challenges in automatic validation. In this paper, we introduce and define
LLM4nl2post as the problem of translating natural language comments into
programmatically checkable postconditions by leveraging Large Language Models
(LLMs). Our work proposes and validates metrics for assessing the correctness
and completeness of postconditions derived from natural language, offering an
initial step in systematizing the LLM4nl2post problem. Through an empirical
and qualitative evaluation on two benchmarks in different mainstream
programming languages, we find that LLMs are adept at translating natural
language descriptions to formulate non-trivial postconditions that accurately
capture programming intent. Our study also finds that LLM-generated
postconditions can exhibit high discriminative power: we generate
postconditions via LLM4nl2post that are able to discriminate 70 real-world
historical bugs from their fixes in industrial-scale Java projects. These
findings underscore the feasibility and promise of leveraging natural language
documentation into executable and checkable specifications. Our research
highlights the possibility of LLMs acting as a bridge between informal
language descriptions and formal code specifications, such that natural
language comments can be used effectively to improve software validation and
bug detection.

##### Acknowledgements.

The authors acknowledge valuable discussions with several members of Microsoft
Research (MSR) around the topic including Tom Ball, Madanlal Musuvathi, Nikhil
Swamy and Shan Lu.

## References

  * (1)
  * Arcuri (2008) Andrea Arcuri. 2008.  On the automation of fixing software bugs. In _Companion of the 30th international conference on Software engineering_. 1003–1006.
  * AWS (2023) Amazon AWS. 2023.  Amazon CodeWhisperer.  Accessed September 27, 2023. https://aws.amazon.com/codewhisperer/.
  * Blasi et al. (2018) Arianna Blasi, Alberto Goffi, Konstantin Kuznetsov, Alessandra Gorla, Michael D Ernst, Mauro Pezzè, and Sergio Delgado Castellanos. 2018.  Translating code comments to procedure specifications. In _Proceedings of the 27th ACM SIGSOFT international symposium on software testing and analysis_. 242–253.
  * Bowen et al. (1993) Jonathan P Bowen, Peter T Breuer, and Kevin C Lano. 1993.  Formal specifications in software maintenance: From code to Z++ and back again.  _Information and Software Technology_ 35, 11-12 (1993), 679–690.
  * Chalin et al. (2006) Patrice Chalin, Joseph R Kiniry, Gary T Leavens, and Erik Poll. 2006.  Beyond assertions: Advanced specification and verification with JML and ESC/Java2. In _Formal Methods for Components and Objects: 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised Lectures 4_. Springer, 342–363.
  * Chen et al. (2021) Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde de Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, et al. 2021\.  Evaluating large language models trained on code.  _arXiv preprint arXiv:2107.03374_ (2021).
  * Cousot et al. (2012) Patrick M Cousot, Radhia Cousot, Francesco Logozzo, and Michael Barnett. 2012.  An abstract interpretation framework for refactoring with application to extract methods with contracts. In _Proceedings of the ACM international conference on Object oriented programming systems languages and applications_. 213–232.
  * Dijkstra and Scholten (1990) Edsger W Dijkstra and Carel S Scholten. 1990.  The strongest postcondition.  _Predicate Calculus and Program Semantics_ (1990), 209–215.
  * Dinella et al. (2022) Elizabeth Dinella, Gabriel Ryan, Todd Mytkowicz, and Shuvendu K Lahiri. 2022.  Toga: A neural method for test oracle generation. In _Proceedings of the 44th International Conference on Software Engineering_. 2130–2141.
  * Ernst et al. (1999) Michael D Ernst, Jake Cockrell, William G Griswold, and David Notkin. 1999.  Dynamically discovering likely program invariants to support program evolution. In _Proceedings of the 21st international conference on Software engineering_. 213–224.
  * Fakhoury et al. (2023) Sarah Fakhoury, Saikat Chakraborty, Madan Musuvathi, and Shuvendu K Lahiri. 2023.  Towards Generating Functionally Correct Code Edits from Natural Language Issue Descriptions.  _arXiv preprint arXiv:2304.03816_ (2023).
  * Garg et al. (2016) Pranav Garg, Daniel Neider, P. Madhusudan, and Dan Roth. 2016.  Learning invariants using decision trees and implication counterexamples. In _Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016_ , Rastislav Bodík and Rupak Majumdar (Eds.). ACM, 499–512.  https://doi.org/10.1145/2837614.2837664
  * GitHub (2023) GitHub. 2023.  GitHub Copilot.  Accessed September 27, 2023. https://github.com/features/copilot/.
  * Goffi et al. (2016) Alberto Goffi, Alessandra Gorla, Michael D Ernst, and Mauro Pezzè. 2016.  Automatic generation of oracles for exceptional behaviors. In _Proceedings of the 25th international symposium on software testing and analysis_. 213–224.
  * He (2019) Hao He. 2019.  Understanding source code comments at large-scale. In _Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering_. 1217–1219.
  * Hsu and Lachenbruch (2014) Henry Hsu and Peter A Lachenbruch. 2014.  Paired t test.  _Wiley StatsRef: statistics reference online_ (2014).
  * Jackson (1992) Daniel Jackson. 1992.  _Aspect, a formal specification language for detecting bugs_.  Ph. D. Dissertation. Citeseer.
  * Jia and Harman (2010) Yue Jia and Mark Harman. 2010.  An analysis and survey of the development of mutation testing.  _IEEE transactions on software engineering_ 37, 5 (2010), 649–678.
  * Just et al. (2014) René Just, Darioush Jalali, and Michael D Ernst. 2014.  Defects4J: A database of existing faults to enable controlled testing studies for Java programs. In _Proceedings of the 2014 international symposium on software testing and analysis_. 437–440.
  * Key et al. (2022) Darren Key, Wen-Ding Li, and Kevin Ellis. 2022.  I speak, you verify: Toward trustworthy neural program synthesis.  _arXiv preprint arXiv:2210.00848_ (2022).
  * Kocetkov et al. (2022) Denis Kocetkov, Raymond Li, Loubna Ben Allal, Jia Li, Chenghao Mou, Carlos Muñoz Ferrandis, Yacine Jernite, Margaret Mitchell, Sean Hughes, Thomas Wolf, et al. 2022\.  The stack: 3 tb of permissively licensed source code.  _arXiv preprint arXiv:2211.15533_ (2022).
  * Lahiri et al. (2022) Shuvendu K Lahiri, Aaditya Naik, Georgios Sakkas, Piali Choudhury, Curtis von Veh, Madanlal Musuvathi, Jeevana Priya Inala, Chenglong Wang, and Jianfeng Gao. 2022.  Interactive code generation via test-driven user-intent formalization.  _arXiv preprint arXiv:2208.05950_ (2022).
  * Lampinen et al. (2022) Andrew K. Lampinen, Ishita Dasgupta, Stephanie C. Y. Chan, Kory Matthewson, Michael Henry Tessler, Antonia Creswell, James L. McClelland, Jane X. Wang, and Felix Hill. 2022.  Can language models learn from explanations in context?  arXiv:2204.02329 [cs.CL]
  * Leino (2010) K Rustan M Leino. 2010.  Dafny: An automatic program verifier for functional correctness. In _Logic for Programming, Artificial Intelligence, and Reasoning: 16th International Conference, LPAR-16, Dakar, Senegal, April 25–May 1, 2010, Revised Selected Papers 16_. Springer, 348–370.
  * Leitner et al. (2007) Andreas Leitner, Ilinca Ciupa, Manuel Oriol, Bertrand Meyer, and Arno Fiva. 2007.  Contract driven development= test driven development-writing test cases. In _Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering_. 425–434.
  * Lemieux et al. (2023) Caroline Lemieux, Jeevana Priya Inala, Shuvendu K Lahiri, and Siddhartha Sen. 2023.  CODAMOSA: Escaping coverage plateaus in test generation with pre-trained large language models. In _International conference on software engineering (ICSE)_.
  * Li et al. (2023) Raymond Li, Loubna Ben Allal, Yangtian Zi, Niklas Muennighoff, Denis Kocetkov, Chenghao Mou, Marc Marone, Christopher Akiki, Jia Li, Jenny Chim, et al. 2023\.  StarCoder: may the source be with you!  _arXiv preprint arXiv:2305.06161_ (2023).
  * Liu et al. (2023) Jiawei Liu, Chunqiu Steven Xia, Yuyao Wang, and Lingming Zhang. 2023.  Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation.  _37th cconference on Neural Information processing Systems (NeurIPS), 2023_ (2023).  https://arxiv.org/abs/2305.01210
  * Mastropaolo et al. (2022) Antonio Mastropaolo, Nathan Cooper, David Nader Palacio, Simone Scalabrino, Denys Poshyvanyk, Rocco Oliveto, and Gabriele Bavota. 2022.  Using transfer learning for code-related tasks.  _IEEE Transactions on Software Engineering_ 49, 4 (2022), 1580–1598.
  * Mike et al. (2004) B Mike, K Rustan M Leino, and S Wolfram. 2004.  The Spec# programming system: An overview. In Construction and Analysis of Safe, Secure, and Interoperable Smart devices (CASSIS)” volume 3362 of Lecture Notes in Computer Science.
  * Molina et al. (2021) Facundo Molina, Pablo Ponzio, Nazareno Aguirre, and Marcelo Frias. 2021.  EvoSpex: An evolutionary algorithm for learning postconditions. In _2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE)_. IEEE, 1223–1235.
  * Nijkamp et al. (2022) Erik Nijkamp, Bo Pang, Hiroaki Hayashi, Lifu Tu, Huan Wang, Yingbo Zhou, Silvio Savarese, and Caiming Xiong. 2022.  Codegen: An open large language model for code with multi-turn program synthesis.  _arXiv preprint arXiv:2203.13474_ (2022).
  * Olausson et al. (2023) Theo X Olausson, Jeevana Priya Inala, Chenglong Wang, Jianfeng Gao, and Armando Solar-Lezama. 2023.  Demystifying GPT Self-Repair for Code Generation.  _arXiv preprint arXiv:2306.09896_ (2023).
  * Ostroff et al. (2004) Jonathan S Ostroff, David Makalsky, and Richard F Paige. 2004.  Agile specification-driven development. In _International Conference on Extreme Programming and Agile Processes in Software Engineering_. Springer, 104–112.
  * Ouyang et al. (2022) Long Ouyang, Jeffrey Wu, Xu Jiang, Diogo Almeida, Carroll Wainwright, Pamela Mishkin, Chong Zhang, Sandhini Agarwal, Katarina Slama, Alex Ray, et al. 2022\.  Training language models to follow instructions with human feedback.  _Advances in Neural Information Processing Systems_ 35 (2022), 27730–27744.
  * Pandita et al. (2012) Rahul Pandita, Xusheng Xiao, Hao Zhong, Tao Xie, Stephen Oney, and Amit Paradkar. 2012.  Inferring method specifications from natural language API descriptions. In _2012 34th international conference on software engineering (ICSE)_. IEEE, 815–825.
  * Pei et al. (2023) Kexin Pei, David Bieber, Kensen Shi, Charles Sutton, and Pengcheng Yin. 2023.  Can Large Language Models Reason about Program Invariants?  (2023).
  * Pfeiffer (2020) Rolf-Helge Pfeiffer. 2020.  What constitutes software? An empirical, descriptive study of artifacts. In _Proceedings of the 17th International Conference on Mining Software Repositories_. 481–491.
  * Rutledge et al. (2014) Richard Rutledge, Sheryl Duggins, Dan Lo, and Frank Tsui. 2014.  Formal specification-driven development. In _Proceedings of the International Conference on Software Engineering Research and Practice (SERP)_. The Steering Committee of The World Congress in Computer Science, Computer …, 1.
  * Ryan et al. (2020) Gabriel Ryan, Justin Wong, Jianan Yao, Ronghui Gu, and Suman Jana. 2020.  CLN2INV: Learning Loop Invariants with Continuous Logic Networks. In _International Conference on Learning Representations_.
  * Sharma and Aiken (2016) Rahul Sharma and Alex Aiken. 2016.  From invariant checking to invariant inference using randomized search.  _Formal Methods in System Design_ 48 (2016), 235–256.
  * Shoham et al. (2007) Sharon Shoham, Eran Yahav, Stephen Fink, and Marco Pistoia. 2007.  Static specification mining using automata-based abstractions. In _Proceedings of the 2007 International Symposium on Software Testing and Analysis_. 174–184.
  * Su et al. (2023) Yiming Su, Chengcheng Wan, Utsav Sethi, Shan Lu, Madan Musuvathi, and Suman Nath. 2023.  HotGPT: How to Make Software Documentation More Useful with a Large Language Model?. In _Proceedings of the 19th Workshop on Hot Topics in Operating Systems_. 87–93.
  * Swamy et al. (2011) Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, and Jean Yang. 2011.  Secure Distributed Programming with Value-Dependent Types. In _Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming_ (Tokyo, Japan) _(ICFP ’11)_. Association for Computing Machinery, New York, NY, USA, 266–278.  https://doi.org/10.1145/2034773.2034811
  * Tabnine (2023) Tabnine. 2023.  Tabnine Code Completion.  Accessed September 27, 2023. https://www.tabnine.com/.
  * Tan et al. (2007) Lin Tan, Ding Yuan, Gopal Krishna, and Yuanyuan Zhou. 2007.  /* iComment: Bugs or bad comments?*. In _Proceedings of twenty-first ACM SIGOPS symposium on Operating systems principles_. 145–158.
  * Tan et al. (2011) Lin Tan, Yuanyuan Zhou, and Yoann Padioleau. 2011.  aComment: mining annotations from comments and code to detect interrupt related concurrency bugs. In _Proceedings of the 33rd international conference on software engineering_. 11–20.
  * Tan et al. (2012) Shin Hwei Tan, Darko Marinov, Lin Tan, and Gary T Leavens. 2012.  @ tcomment: Testing javadoc comments to detect comment-code inconsistencies. In _2012 IEEE Fifth International Conference on Software Testing, Verification and Validation_. IEEE, 260–269.
  * Tufano et al. (2020) Michele Tufano, Dawn Drain, Alexey Svyatkovskiy, Shao Kun Deng, and Neel Sundaresan. 2020.  Unit Test Case Generation with Transformers and Focal Context.  https://doi.org/10.48550/ARXIV.2009.05617
  * Tufano et al. (2022) Michele Tufano, Dawn Drain, Alexey Svyatkovskiy, and Neel Sundaresan. 2022.  Generating Accurate Assert Statements for Unit Test Cases using Pretrained Transformers. In _IEEE/ACM International Conference on Automation of Software Test, AST@ICSE 2022, Pittsburgh, PA, USA, May 21-22, 2022_. ACM/IEEE, 54–64.  https://doi.org/10.1145/3524481.3527220
  * Vikram et al. (2023) Vasudev Vikram, Caroline Lemieux, and Rohan Padhye. 2023.  Can Large Language Models Write Good Property-Based Tests?  _arXiv preprint arXiv:2307.04346_ (2023).
  * Wei et al. (2022) Jason Wei, Yi Tay, Rishi Bommasani, Colin Raffel, Barret Zoph, Sebastian Borgeaud, Dani Yogatama, Maarten Bosma, Denny Zhou, Donald Metzler, et al. 2022\.  Emergent Abilities of Large Language Models.  _Transactions on Machine Learning Research_ (2022).
  * Wei et al. (2023) Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Brian Ichter, Fei Xia, Ed Chi, Quoc Le, and Denny Zhou. 2023.  Chain-of-Thought Prompting Elicits Reasoning in Large Language Models.  arXiv:2201.11903 [cs.CL]
  * Yao et al. (2020) Jianan Yao, Gabriel Ryan, Justin Wong, Suman Jana, and Ronghui Gu. 2020.  Learning nonlinear loop invariants with gated continuous logic networks. In _Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation_. 106–120.
  * Zhong et al. (2009) Hao Zhong, Lu Zhang, Tao Xie, and Hong Mei. 2009.  Inferring resource specifications from natural language API documentation. In _2009 IEEE/ACM International Conference on Automated Software Engineering_. IEEE, 307–318.
  * Zhou et al. (2023) Denny Zhou, Nathanael Schärli, Le Hou, Jason Wei, Nathan Scales, Xuezhi Wang, Dale Schuurmans, Claire Cui, Olivier Bousquet, Quoc Le, and Ed Chi. 2023.  Least-to-Most Prompting Enables Complex Reasoning in Large Language Models.  arXiv:2205.10625 [cs.AI]
  * Zhou et al. (2017) Yu Zhou, Ruihang Gu, Taolue Chen, Zhiqiu Huang, Sebastiano Panichella, and Harald Gall. 2017.  Analyzing APIs documentation and code to detect directive defects. In _2017 IEEE/ACM 39th International Conference on Software Engineering (ICSE)_. IEEE, 27–37.

##  Appendix A Appendix

We present an additional metric for postcondition completeness: test-set
completeness. We also demonstrate the impact of benchmark quality on our
correctness metric by comparing postcondition test-set correctness between
EvalPlus and HumanEval, two benchmarks that have the same problems, but
drastically different numbers of tests.

###  A.1. Test-set completeness for test mutants

Given a set of code mutants $\it CM$, one can formulate a stronger
completeness measure compared to code-completeness-score (see section 3.1.4)
as follows. Let us collect the set of incorrect test outputs by executing all
the code mutants on each input $i\in{\it T}$ and collect the outputs that
differ from ${\it r}$ on the particular input $i$. We can define a mutation
score that measures the fraction of such incorrect outputs that fail the
postcondition.

More precisely, let us define the set of incorrect input-output mutants as
follows:

$\it TestMutants({\it r},{\it T},\it CM)\doteq\bigcup_{i\in{\it
T}}\\{(i,o^{\prime})\ |\ \exists c\in\it CM:o^{\prime}==c(i)\neq{\it r}(i)\\}$

We define the test-set-completeness score of ${\it post}$ under a set of test-
mutants ${\it TM}$ as follows:

$\textit{test-completeness-score}({\it post},{\it
TM})\doteq|\\{(i,o^{\prime})\in{\it TM}\ |\ \it eval(post,(i,o^{\prime}))==\it
false\\}|/|{\it TM}|$

It is not hard to see for a given problem $\langle{\it nl},{\it r},{\it
T}\rangle$ and code mutants $\it CM$, if a correct postcondition ${\it post}$
kills all the test mutants in $\it TestMutants({\it r},{\it T},\it CM)$, then
${\it post}$ kills all the code mutants in $\it CM$. This follows because each
code mutants $c\in\it CM$ contributes at least one test mutant in $\it
TestMutants$. Interestingly, the other direction does not hold: killing all
the code mutants does not ensure that all the test mutants will be killed.
Consider the following example where the ${\it nl}$ corresponds to ”increment
a number”. Let ${\it r}\doteq\lambda x:x+1$ be the reference solution, with
${\it T}\doteq\\{0,1,2\\}$ and let $\it CM\doteq\\{\lambda x:1,\lambda
x:2\\}$. The corresponding set of test mutants $\it
TestMutants\doteq\\{(1,1),(2,1),(0,2),(2,2)\\}$. The first two test mutant
comes from the first code mutant $\lambda x:1$ and the latter two from the
second code mutant $\lambda x:2$. Consider the postcondition ${\it
post}\doteq{\it ret}>x$ that states that the returned value ${\it ret}$ should
be greater than the input $x$. This postcondition removes at least one test
mutant for both the code mutant thereby achieving a score of 1 for the bug-
completeness-score for code mutants. However, it fails to remove the test
mutant $(0,2)$ that comes from the second code mutant; therefore it only
achieves a score of 3/4 (or $0.75$) for the test-completeness score for test
mutants.

⬇

1 def has_close_elements(nums: List[float], threshold: float):

2 """ Check if in a given list of numbers, are any two numbers

3 closer to each other than a given threshold."""\end{Python}

4 \caption{Problem 0 from \humanevalplus{}, truncated slightly for space
\label{tab:diverge:a}}

5 \end{subfigure}

6

7

8 \centering

9 \begin{subfigure}{\textwidth}

10 \centering

11 \begin{tabular}{@{}lrr@{}}

12\toprule

13 & \multicolumn{2}{c}{Completeness} \\\

14\multirow{-2}{*}{Postcondition} & Test suite & Bug \\\ \midrule

15\pyinline{assert isinstance(return_val, bool)} &
\cellcolor[HTML]{CBCEFB}\textbf{44.7 \%} & 16.7 \% \\\

16\begin{tabular}[c]{@{}l@{}}

17\pyinline{assert not return_val or any(abs(nums{[}i{]} - nums{[}j{]}) <
threshold} \\\ \hspace{1cm} \pyinline{for i in range(len(nums)) for j in
range(i+1, len(nums)))}\end{tabular} &

18 11.3 \% &

19 \cellcolor[HTML]{CBCEFB}\textbf{66.7 \%} \\\ \bottomrule

20\end{tabular}

21\caption{Table showing two correct postconditions for \humanevalplus{}
problem 0 generated by \GPTfour{}. While both correct, notice that the test
suite and bug completeness metrics are incomparable. \label{tab:diverge:b} }

22

23 \end{subfigure}

24\caption{ \label{tab:diverge}}

25\end{figure}

26

27While the Boolean metric for test-mutant completeness (i.e., \textit{test-
completeness-score} == 1) is strictly stronger than the Boolean metric for
bug-mutant completeness (i.e., \textit{code-completeness-score} == 1), the
absolute metrics \textit{test-completeness-score} vs. \textit{bug-
completeness-score} are incomparable.

28These metrics depend on the number of code and test mutants for a given
example, and may differ from each other considerably.

29Some examples may only have a few code-mutants generated that induce several
different test-mutants per mutant, and other examples may have several code-
mutants that each generate only a single differing test-mutant.

30Moreover, a specific postcondition may distinguish between a relatively
small number of code mutants while distinguishing several test mutants and
vice versa.

31

32Table~\ref{tab:diverge} illustrates an example from \humanevalplus{}
(Fig~\ref{tab:diverge:a}), and two correct postconditions generated by
\GPTfour{} (Fig~\ref{tab:diverge:b}) .

33The first postcondition distinguishes only a small fraction of code mutants
($16.7\%$) each of which induce several test mutants that are also
distinguished ($44.7\%)$.

34On the other hand, the second postconditions distinguishes a large fraction
of code-mutants ($66.7\%$) but only distinguishes a few test mutants
($11.3\%$) where they differ from the reference solution.

35In this paper, we only focus on \textit{code-completeness-score} and reserve
comparing these metrics overall for future work.

36

37

38\subsection{HumanEval vs. EvalPlus}

39

40

41\begin{figure}[h!]

42 \centering

43 \includegraphics[width=\linewidth]{images/appendix-2.pdf}

44 \caption{Comparing test-set correctness for \humaneval{} vs
\humanevalplus{} benchmarks. This represents results for the \texttt{base}
prompt with out the reference solution (e.g., natural language specification
only).

45 \label{fig:humanEvalVsPlus}}

46

47

48\end{figure}

49

50

51Recall that \humanevalplus{} improves the quality of the test-suite $\tests$
over the base \humaneval{} benchmark set (see
Section~\ref{subsec:humanEvalBenchmark}).

52Given an example $\langle \nl, \refr, \tests \rangle$, a postcondition is
{\it spurious} if it is test-set correct for $\tests$ but fails to be correct
for all legal inputs with respect to reference implementation $\refr$.

53In our manual qualitative analysis over the random sample, we identified
only a single problem in \humanevalplus{} benchmark that generated with
spurious postconditions.

54Figure~\ref{fig:humanEvalVsPlus} illustrates that several additional
postconditions that are not test-set correct for \humanevalplus{} are marked
as correct for \humaneval{}.

55Clearly, these postconditions are guaranteed to be spurious since there
exists a legal input (from the test suite of \humanevalplus{}) for which the
postcondition fails on $\refr$. This difference is non-trivial for all models,
ranging between 3-7\% for \texttt{accept@10}. We focus on \texttt{accept@10}
because the existence of even one incorrect postcondition for a given problem
indicates that the test-suite for that problem is under-specified: as reported
in Section~\ref{subsec:humanEvalCorrectness}, for \GPTfour{} $7\%$ of all the
generated postconditions are spurious with respect to under-specified test set
in \humaneval{} with respect to the test sets in \humanevalplus{}. These
differences demonstrate how the quality of a benchmark’s test-suite can impact
ability of our proposed test-set correctness metric to reasonably approximate
true post-condition correctness.’