SEMBridge: Tagless-Final Program Semantics with Weakest-Precondition and Bounded-Checking Interpretations
For software engineers using formal methods, SEMBridge provides a compact architecture to synchronize executable semantics, weakest-precondition artifacts, and bounded validation without separate traversals.
SEMBridge introduces a tagless-final framework that generates both weakest-precondition and bounded-checking interpretations from the same executable object programs, keeping semantics synchronized. Across five example programs, the same definitions generated executable state transformers and verification conditions that passed bounded checking over domains up to 729 states.
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.