Specify What? a Case-Study Using GPT-4 and Formal Methods for Specification Synthesis

Abstract

Formal specifications are supposed to unambigu- ously describe the behaviour of (parts of) pro- grams and are usually provided as extra annota- tions of the program code. The intention is both to document the code and to be able to automati- cally check compliance of programs using formal methods tools. Writing good specifications can however be both difficult and time-consuming for the programmer. In this case-study, we investigate how GPT-4 can help with the task. We propose a neuro-symbolic integration, by which we aug- ment the LLM prompts with outputs from two formal methods tools in the Frama-C ecosystem (Pathcrawler and EVA), and produce C program annotations in the specifications language ACSL. We demonstrate how this impacts the quality of annotations: information about input/output ex- amples from Pathcrawler produce more context- aware annotations, while the inclusion of EVA reports yields annotations more attuned to run- time errors.