开发与证明一体化的编程范式

以下摘要由 AI 根据胶片自动生成。

针对高安全软件开发中实现语言、规约语言和证明工具相互割裂的问题，本报告提出开发与证明一体化的编程范式，以类 C 语言（C*）在同一环境中统一编写功能代码、规约代码与证明代码。程序员通过前后条件、循环不变式和程序断言等契约机制标注代码，编译器负责检查这些标注的正确性，无需切换工具链。短期方案基于 VST-A 框架，将符号执行与 Coq 中的分离逻辑自动衔接，支持归纳法、等式规约函数和 SMT 辅助证明。