A Hoare Logic for Domain Specification (Full Version)
Eduard Kamburjan, Dilian Gurov
TL;DR
This work presents a two-tier Hoare logic that couples domain knowledge encoded in description logics with imperative program verification through semantic lifting $\\mu$ and specification lifting $\\hat{\\mu}$. A kernel-generator $\\alpha_{\\mathbf{K}}$ and abductive/deductive mechanisms enable deriving and recovering domain constraints, ensuring compatibility between domain and state assertions. The calculus is procedure-modular and sound, featuring rules such as (pre-lift), (post-lift), (pre-core), (post-core), (var), and (contract) to verify that domain post-conditions hold when program state post-conditions do. A car-assembly motivating example demonstrates practical integration of domain ontologies with verification and points to future work on expressivity, decidability, and scalability of the lifting-based approach.
Abstract
Programs must be correct with respect to their application domain. Yet, the program specification and verification approaches so far only consider correctness in terms of computations. In this work, we present a two-tier Hoare Logic that integrates assertions for both implementation and domain. For domain specification, we use description logics and semantic lifting, a recently proposed approach to interpret a program as a knowledge graph. We present a calculus that uses translations between both kinds of assertions, thus separating the concerns in specification, but enabling the use of description logic in verification.