基于大语言模型的程序形式化规范生成与验证方法及系统

本发明公开了基于大语言模型的程序形式化规范生成与验证方法及系统，涉及程序代码形式化验证领域，本发明依托大语言模型强大的计算能力，在短时间内高效地生成大量的形式化规范，显著提升了形式化规范生成的效率；同时，融合静态验证和模糊测试两种方法对生成的形式化规范进行验证，将静态验证失败的规范分为静态验证错误规范和超时规范，针对超时规范进一步进行模糊测试，减少了因单一验证方式的能力限制对所述待验证规范产生错误反馈而引发的形式化规范生成不充分的问题，提高了形式化规范验证的成功率。