AI 中文总结
该研究提出面向计算机科学教育的VeGo系统，可直接验证标准Go程序，整合多种形式化验证技术，对比其他语言论证Go的优势，经教育教材评估并规划了形式并发规约的路线图。
AI 中文摘要
随着AI编码代理推动形式化方法快速变得可及且实用，当前重点转向辅助开发者和学生生成规约。利用原生HMX/SSA验证器可提供带有严格数学约束的支持。我们提出VeGo（Verified Go，已验证的Go），这是一种演绎形式化验证系统，可实现对标准Go源代码的直接验证。VeGo整合了Hoare式契约、循环不变量、整数变体、良基递归度量、块级作用域不变量以及带素变量的等式推理链，所有这些均以非侵入式Go注释形式呈现。我们详述了语言选择的理由，论证Go相比C、C++、Java和Rust是理想的平衡选择，策略性采用了Go的原生多返回值特性。我们详述了工具架构，利用静态单赋值（SSA）形式与一阶函数式编程之间的理论等价性来注释代码、消除开区间量词的语法糖、添加Reynolds的skip语句、提供最弱前置条件演算以及原生Hindley-Milner约束推理，还可基于SSA形式进行验证条件求解。我们通过与类型推理的明确类比，形式化了契约精度检查（最弱前置条件与最强后置条件）。最后，我们针对教育教材对VeGo进行评估，并概述了使用认知时态逻辑进行形式并发规约的路线图。
英文摘要
As formal methods are rapidly becoming accessible and practical due to AI coding agents, priority passes to assisting developers and students in generating specifications. Leveraging native HMX/SSA verifiers provide that support with rigorous mathematical guardrails. We present VeGo (Verified Go), a deductive formal verification system that enables direct verification of standard Go source code. VeGo incorporates Hoare-style contracts, loop invariants and integer variants, well-founded recursive measures, block-level scope invariants, and equational reasoning chains with primed variables directly as non-intrusive Go comments. We detail the language selection rationale justifying Go as an ideal balance over C, C++, Java, and Rust, strategically adopting Go's native multiple return values. We detail the tool architecture, exploiting the theoretical equivalence between Static Single Assignment (SSA) form and first-order functional programming to annotate code, desugar of clopen interval quantifiers, add Reynolds' skip statement, provide weakest precondition calculus, and native Hindley-Milner constraint inference, and verification condition resolution over the SSA form. We formalize contract-precision checking (weakest precondition vs. strongest postcondition) using an explicit analogy to type inference. Finally, we evaluate VeGo across educational textbooks and outline a roadmap for formal concurrency specifications using epistemic temporal logic.
Comments13 pages + 2 pages of references, 5 code displays, ancillary reference manual for VeGo
