Supplementary Methodology Details

The figure on the left illustrates all kinds of natural language guidance provided to the LLM during the conversation-driven specification generation process. We summarized several types of frequently emerging errors reported by OpenJML, and manually wrote natural language guidance on how to fix them. For each kind of error, we provide guidance in natural language to facilitate the model in generating correct specifications more easily. The guidance information is also provided in the figure below. Upon encountering these types of verification failures reported by the verifier, we will insert corresponding guidance information into the prompt to assist the model in resolving the issues.