Multi-perspective Correctness of Programs

Traditionally, programs are formally specified and verified with respect to their computational domain, disregarding the domain in which they are to be applied. This, however, is inadequate for programs that simulate processes in a specific application domain, or programs that generate data that must conform to external, domain-specific specifications. Such programs need also to be correct with respect to their application domain. This work presents a Hoare Logic that manages two different perspectives on a program during a correctness proof: the computational view and the domain view. This enables us to specify the correctness of a program in terms of the domain without referring to the computational details, but at the same time to interpret failed proof attempts in the domain. For domain specification, we illustrate the use of description logics and base our approach on semantic lifting, an 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.