SEMBridge: Tagless-Final Program Semantics with Weakest-Precondition and Bounded-Checking Interpretations
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Weighted Programming
We study weighted programming, a programming paradigm for specifying mathematical models. More specifically, the weighted programs we investigate are like usual imperative programs with two additional features: (1) nonde…
Probabilistic ProgrammingThe Hoare-fol Tool
This document presents the tool named ''Application of Hoare Logic and Dijkstra's Weakest Proposition Calculus to Biological Regulatory Networks Using Path Programs with Branching First-Order Logic Operators'' or Hoare-f…
TranslationArgument Ranking with Categoriser Function
Recently, ranking-based semantics is proposed to rank-order arguments from the most acceptable to the weakest one(s), which provides a graded assessment to arguments. In general, the ranking on arguments is derived from …
LLMs and Fuzzing in Tandem: A New Approach to Automatically Generating Weakest Preconditions
The weakest precondition (WP) of a program describes the largest set of initial states from which all terminating executions of the program satisfy a given postcondition. The generation of WPs is an important task with p…
Deep Learning-based Real-time Smartphone Pose Detection for Ultra-wideband Tagless Gate
As commercial interest in proximity services increased, the development of various wireless localization techniques was promoted. In line with this trend, Ultra-wideband (UWB) is emerging as a promising solution that can…