  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.
