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.

翻译：形式化方法为程序行为提供了严谨的论证，但实际软件工程通常通过可执行库、测试和增量设计来运作。本文提出SEMBridge，这是一个小型无标签最终框架，用于从相同的可执行目标程序生成最弱前置条件和有界检查解释。程序语义不再固定于单一抽象语法树并编写单独遍历，而是通过语义接口一次性编写目标程序，然后解释为多种含义：可读代码、具体执行、谓词转换器、有界反例搜索以及未来的证明助手或SMT后端。该Python原型实现了一个包含赋值、条件、假设和断言的无循环命令式核心。在五个示例程序中，相同的无标签最终定义为最多729个状态的域生成了可执行状态转换器和通过有界检查的验证条件。本贡献并非Scala代码生成系统或新验证器，而是一种紧凑架构，用于保持可执行语义、最弱前置条件产物和有界验证的同步。