一个无需标签的框架，让同一段代码同时支持运行和验证
SEMBridge: Tagless-Final Program Semantics with Weakest-Precondition and Bounded-Checking Interpretations
- 用统一接口编写程序，自动生成可执行代码与验证条件
- 5个示例在729状态内通过边界检查，验证条件正确
- 适合需要代码与验证同步的开发与形式化验证场景
形式化方法能精确描述程序行为，但实际工程常依赖可执行库、测试和增量设计。本文提出SEMBridge，一个轻量级无标签终态框架，可从同一可执行程序生成最弱前提（weakest-precondition）与有界检查解释。程序仅需定义一次，即可被解释为可读代码、具体执行、谓词变换器、有界反例搜索，以及未来对接证明助手或SMT求解器。原型基于Python实现无循环的命令式核心，包含赋值、条件、假设和断言。在五个示例中，相同无标签终态定义生成的可执行状态转换器与验证条件，在最多729个状态的域上通过了有界检查。贡献不在于新代码生成系统或验证器，而是一种紧凑架构，确保可执行语义、最弱前提产物与有界验证始终一致。
原文摘要 · Abstract (English)
Formal methods provide rigorous accounts of program behavior, but practical software engineering often works through executable libraries, tests, and incremental design. This paper presents SEMBridge, a small tagless-final framework for generating weakest-precondition and bounded-checking interpretations from the same executable object programs. Instead of committing a program semantics to one abstract syntax tree and then writing separate traversals, object programs are written once against a semantic interface and interpreted into multiple meanings: readable code, concrete execution, predicate transformers, bounded counterexample search, and future proof-assistant or SMT back ends. The Python prototype implements a loop-free imperative core with assignments, conditionals, assumptions, and assertions. Across five example programs, the same tagless-final definitions generated executable state transformers and verification conditions that passed bounded checking over domains up to 729 states. The contribution is not a Scala code-generation system or a new verifier, but a compact architecture for keeping executable semantics, weakest-precondition artifacts, and bounded validation synchronized.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。