Open access
Aug 2026
Assertions for Free: Transferring Invariants from Algorithm to Implementation Proofs (Functional Pearl)
This pearl shows how a clean separation can be achieved within the two-layer method by combining two simple ideas: expressing implementation correctness as a relational Hoare quadruple, and introducing assertion annotations into the abstract program to capture key invariants.
Shushu Wu, Chengxi Yang, Xi-Wei Wu et al.
· Proc. ACM Program. Lang. · 0 citations