Content area
Declarative specifications have a vital role to play in developing safe and dependable software systems. Writing specifications correctly, however, remains particularly challenging. This paper presents a controlled experiment using large language models (LLMs) to write declarative formulas in the well-known language Alloy. Our use of LLMs is four-fold. One, we employ LLMs to write complete Alloy formulas from given natural language descriptions (in English). Two, we employ LLMs to create alternative but equivalent formulas in Alloy with respect to the given Alloy formulas. Three, we employ LLMs to determine whether the given Alloy formulas match the given natural language descriptions. Four, we employ LLMs to complete sketches of Alloy formulas and populate the holes in the sketches by synthesizing Alloy expressions and operators so that the completed formulas accurately represent the desired properties (that are given in natural language) and/or with respect to given tests. We conduct the experimental evaluation using 21 well-studied subject specifications and employ two popular LLMs, namely ChatGPT and Claude. The experimental results show that the LLMs generally perform well in synthesizing complete Alloy formulas from input properties given in natural language or in Alloy, and are able to enumerate multiple unique solutions. Moreover, the LLMs are also able to complete given sketches of simple Alloy formulas with respect to natural language descriptions of desired properties and/or given tests. We believe LLMs offer a promising advance in our ability to write specifications, and can help make specifications take a pivotal role in software development and enhance our ability to build robust software.