Operational Semantics and Program Verification Using Many-Sorted Hybrid Modal Logic

Abstract

We propose a general framework to allow: (a) specifying the operational semantics of a programming language; and (b) stating and proving properties about program correctness. Our framework is based on a many-sorted system of hybrid modal logic, for which we prove its completeness results. We believe that our approach to program verification improves over the existing approaches within modal logic as (1) it is based on operational semantics which enables a more natural description of the execution than Hoare-style weakest precondition used by dynamic logic; (2) since it is multi-sorted, it allows for a clearer encoding of semantics, with a smaller representational distance to its intended meaning.