Elamur Research⌕
☰
home / papers / 2026 / POSTCONDBENCH: Benchmarking Correctness and Completeness in Formal Postcondition Inference

POSTCONDBENCH: Benchmarking Correctness and Completeness in Formal Postcondition Inference

Paper · 2026 · Gehao Zhang and Juan Zhai

Summary

Automatically generated formal postconditions are hard to evaluate. Most prior checks only ask whether a postcondition holds on a correct implementation, so they miss whether it captures enough of the method's behavior. Completeness has mostly been judged by hand or with brittle string/AST matching on small, synthetic programs. The authors present POSTCONDBENCH, a benchmark of method-level postcondition tasks taken from real open-source Python and Java repositories. Each task includes:

  • a signature, documentation, implementation and tests,
  • implementation mutants,
  • a ground-truth postcondition set built semi-automatically with expert help, written in icontract (Python) or JML (Java).

Correctness is checked by running the tests. Completeness is measured by defect discrimination: a better set rejects more faulty mutants while still holding on correct runs. This avoids having to check equivalence against one canonical specification. The authors evaluate five state-of-the-art LLMs in three generation settings. Models often produce correct postconditions but much less often complete ones. Repository-level dependencies and longer methods widen this gap. The benchmark gives specification-generation research a realistic, automatically scored testbed.

Key points

  • The benchmark has 420 Python/Java tasks from 121 open-source projects. Its code and data are released at github.com/zhang-ge-hao/postcond-bench.
  • Even GPT-5 reaches at most about 17% completeness on Python and 43% on Java.
  • Environment setup used an LLM-driven loop (gpt-o4-mini) that edited config files such as pyproject.toml and pom.xml. Of 10,000 candidate repositories, 941 (9.4%) ended up runnable.
  • Methods were filtered for comment quality (more than 15 English words), non-trivial complexity and high test coverage. Coverage was measured with tools such as JaCoCo and pytest-cov.
  • Comp@1 is stable: dropping half of the LLM-generated mutants shifts the mean by under 4%, with standard deviation ≤0.004.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓University of Massachusetts AmherstAmherst Center · United States106 works · 66,692 citations

 Fields, topics and concepts

📚 Shelves 4The field of science this work belongs to (OpenAlex fields).Computer Science · 16,667 worksArtificial Intelligence · 16,194 worksInformation Systems · 1,437 worksSoftware · 92 works

Cite

Cite as Gehao Zhang and Juan Zhai. 2026. POSTCONDBENCH: Benchmarking Correctness and Completeness in Formal Postcondition Inference. Findings of the Association for Computational Linguistics: ACL 2026.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.18653/v1/2026.findings-acl.1768

@inproceedings{zhang2026postcondbench,
  title = {{POSTCONDBENCH: Benchmarking Correctness and Completeness in Formal Postcondition Inference}},
  author = {Gehao Zhang and Juan Zhai},
  booktitle = {Findings of the Association for Computational Linguistics: ACL 2026},
  year = {2026},
  doi = {10.18653/v1/2026.findings-acl.1768},
  url = {https://doi.org/10.18653/v1/2026.findings-acl.1768}
}

References

43 references, 6 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Meta AI. 2025. Gpt-4o mini: advancing cost-efficient intelligence. Meta. find
  2. 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, pages 213–224. ACM. find
  3. Johannes Henkel, Christoph Reichenbach, and Amer Diwan. 2008. Developing and debugging algebraic specifications for java classes. ACM Transactions on Software Engineering and Methodology (TOSEM), 17(3):1–37. find
  4. Anders Hovmöller. 2016. Mutmut: a python mutation testing system. https://kodare.net/2016/12/01/ mutmut-a-python-mutation-testing-system. html. Blog post on En kodare. ↗
  5. Ruida Hu, Chao Peng, Junjielong Xu, Cuiyun Gao, and 1 others. 2025. Repo2run: Automated building executable environment for code repository at scale. In The Thirty-ninth Annual Conference on Neural Information Processing Systems. find
  6. Md Ashraful Islam, Mohammed Eunus Ali, and Md Rizwan Parvez. 2024. Mapcoder: Multi-agent code generation for competitive problem solving. In Annual Meeting of the Association of Computational Linguistics 2024, pages 4912–4944. Association for Computational Linguistics (ACL). jacoco. 2025. JaCoCo: Ja… find
  7. Naman Jain, King Han, Alex Gu, Wen-Ding Li, Fanjia Yan, Tianjun Zhang, Sida Wang, Armando Solar-Lezama, Koushik Sen, and Ion Stoica. 2024. Livecodebench: Holistic and contamination free evaluation of large language models for code. arXiv preprint arXiv:2403.07974. jhy. 2025. jsoup: the java html par…
  8. Carlos E Jimenez, John Yang, Alexander Wettig, Shunyu Yao, Kexin Pei, Ofir Press, and Karthik Narasimhan. 2024. Swe-bench: Can language models resolve real-world github issues? In 12th International Conference on Learning Representations, ICLR 2024.
  9. Joowani. 2022. binarytree: A python library for studying binary trees. https://github.com/joowani/ binarytree. GitHub repository, accessed 2026-01-06. ↗
  10. René Just, Darioush Jalali, and Michael D Ernst. 2014a. 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, pages 437–440. find
  11. René Just, Darioush Jalali, Laura Inozemtseva, Michael D Ernst, Reid Holmes, and Gordon Fraser. 2014b. Are mutants a valid substitute for real faults in software testing? In Proceedings of the 22nd ACM SIGSOFT international symposium on foundations of software engineering, pages 654–665. find
  12. Keon. 2025. algorithms: Minimal examples of data structures and algorithms in python and other languages. https://github.com/keon/algorithms. GitHub repository, accessed 2026-01-06. ↗
  13. Jens U Kreber and Christopher Hahn. 2021. Generating symbolic reasoning problems with transformer gans. arXiv preprint arXiv:2110.10054. — [arXiv:2110.10054](https://arxiv.org/abs/2110.10054) find
  14. Woosuk Kwon, Zhuohan Li, Siyuan Zhuang, Ying Sheng, Lianmin Zheng, Cody Hao Yu, Joseph Gonzalez, Hao Zhang, and Ion Stoica. 2023. Efficient memory management for large language model serving with pagedattention. In Proceedings of the 29th symposium on operating systems principles, pages 611–626.
  15. Axel van Lamsweerde. 2000. Formal specification: a roadmap. In Proceedings of the Conference on the Future of Software Engineering, pages 147–159. find
  16. Afshan Latif, Farooque Azam, Muhammad Waseem Anwar, and Amina Zafar. 2023. Comparison of leading language parsers–antlr, javacc, sablecc, tree-sitter, yacc, bison. In 2023 13th International Conference on Software Technology and Engineering (ICSTE), pages 7–13. IEEE. find
  17. Gary T Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, Peter Müller, Joseph Kiniry, Patrice Chalin, Daniel M Zimmerman, and 1 others. 2008. Jml reference manual. find
  18. 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. Advances in Neural Information Processing Systems, 36:21558–21572.
  19. Lezhi Ma, Shangqing Liu, Yi Li, Xiaofei Xie, and Lei Bu. 2025. Specgen: Automated generation of formal program specifications via large language models. In 2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE), pages 16–28. IEEE. find
  20. Thomas J McCabe. 1976. A complexity measure. IEEE Transactions on software Engineering, (4):308–320. find
  21. Gemma Team Thomas Mesnard, Cassidy Hardin, Robert Dadashi, Surya Bhupatiraju, Shreya Pathak, L. Sifre, Morgane Riviere, Mihir Kale, J Christopher Love, Pouya Dehghani Tafti, L’eonard Hussenot, Aakanksha Chowdhery, Adam Roberts, Aditya Barua, Alex Botev, Alex Castro-Ros, Ambrose Slone, Am’elie H’elio… find
  22. Frederic P Miller, Agnes F Vandome, and John McBrewster. 2010. Apache Maven. Alpha Press. find
  23. Hoan Anh Nguyen, Robert Dyer, Tien N Nguyen, and Hridesh Rajan. 2014. Mining preconditions of apis in large-scale code corpus. In Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, pages 166–177. ACM. find
  24. Jeremy W Nimmer and Michael D Ernst. 2002. Automatic generation of program specifications. ACM SIGSOFT Software Engineering Notes, 27(4):229– 239. find
  25. OpenAI. 2023. Code interpreter. https://platform.openai.com/docs/guides/ tools-code-interpreter. OpenAI API Documentation. Accessed: 2026-01-06. ↗
  26. OpenAI. 2025. Gpt-5 is here. OpenAI. find
  27. Jiayi Pan, Xingyao Wang, Graham Neubig, Navdeep Jaitly, Heng Ji, Alane Suhr, and Yizhe Zhang. 2025. Training software engineering agents and verifiers with SWE-gym. In Forty-second International Conference on Machine Learning. find
  28. Rahul Pandita, Xusheng Xiao, Hao Zhong, Tao Xie, Stephen Oney, and Amit Paradkar. 2012. Inferring method specifications from natural language API descriptions. In Proceedings of the 34th International Conference on Software Engineering, pages 815–825. IEEE Press. find
  29. Parquery. 2025. icontract. GitHub repository. find
  30. Parquery AG. 2019. icontract documentation: Async. https://icontract.readthedocs.io/ en/latest/async.html. Accessed: 2026-01-05. pytest-dev. 2025. pytest-cov: Coverage plugin for pytest. https://github.com/pytest-dev/ pytest-cov. GitHub repository. python-poetry. 2026. Poetry: Python packaging and d… ↗
  31. Murali Krishna Ramanathan, Ananth Grama, and Suresh Jagannathan. 2007. Static specification inference using predicate mining. In ACM SIGPLAN Notices, pages 123–134. ACM. find
  32. Daniel J Rosenkrantz, Richard E Stearns, and Philip M Lewis, II. 1977. An analysis of several heuristics for the traveling salesman problem. SIAM journal on computing, 6(3):563–581. find
  33. Sharon Shoham, Eran Yahav, Stephen J. Fink, and Marco Pistoia. 2007. Static specification mining using automata-based abstractions. IEEE Transactions on Software Engineering, 34:651–666. find
  34. Bo Wang, Mingda Chen, Youfang Lin, Mike Papadakis, and Jie M Zhang. 2024. An exploratory study on using large language models for mutation testing. CoRR. find
  35. Danning Xie, Yitong Li, Mijung Kim, Hung Viet Pham, Lin Tan, Xiangyu Zhang, and Michael W Godfrey. 2022. Docter: documentation-guided fuzzing for testing deep learning api functions. In Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 176–188. find
  36. Danning Xie, Byoungwoo Yoo, Nan Jiang, Mijung Kim, Lin Tan, Xiangyu Zhang, and Judy S Lee. 2025. How effective are large language models in generating software specifications? In 2025 IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER), pages 1–12. IEEE. find
  37. Zhiyi Xue, Liangguo Li, Senyue Tian, Xiaohong Chen, Pingping Li, Liangyu Chen, Tingting Jiang, and Min Zhang. 2024. Llm4fin: Fully automating llm-powered test case generation for fintech software acceptance testing. In Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing a… find
  38. An Yang, Anfeng Li, Baosong Yang, Beichen Zhang, Binyuan Hui, Bo Zheng, Bowen Yu, Chang Gao, Chengen Huang, Chenxu Lv, and 1 others. 2025. Qwen3 technical report. arXiv preprint arXiv:2505.09388.
  39. John Yang, Carlos E Jimenez, Alexander Wettig, Kilian Lieret, Shunyu Yao, Karthik Narasimhan, and Ofir Press. 2024. Swe-agent: Agent-computer interfaces enable automated software engineering. Advances in Neural Information Processing Systems, 37:50528– 50652.
  40. Hao Yu, Bo Shen, Dezhi Ran, Jiaxin Zhang, Qi Zhang, Yuchi Ma, Guangtai Liang, Ying Li, Qianxiang Wang, and Tao Xie. 2024. Codereval: A benchmark of pragmatic code generation with generative pre-trained models. In Proceedings of the 46th IEEE/ACM International Conference on Software Engineering, page… find
  41. Juan Zhai, Yu Shi, Minxue Pan, Guian Zhou, Yongxiang Liu, Chunrong Fang, Shiqing Ma, Lin Tan, and Xiangyu Zhang. 2020. C2s: translating natural language comments to formal program specifications. In Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium o… find
  42. Shiyu Zhang, Juan Zhai, Bu Lei, Wang Linzhang, and Xuandong Li. 2020. Automated geration of ltl specifications for smart home iot using natural language. In 2020 Design, Automation & Test in Europe Conference & Exhibition (DATE). IEEE. find
  43. Colin Frank Snook. 2001. Exploring the barriers to formal specification. Ph.D. thesis, University of Southampton. find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/zhang-2026-postcondbench-benchmarking-correctness-completeness-formal/