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 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 allows for a more natural description of the execution than Hoare's style weakest precondition used by dynamic logic; (2) being multi-sorted, it allows for a clearer encoding of semantics, with a smaller representational distance to its intended meaning.

翻译：我们提出一个通用框架，以支持：（a）指定编程语言的操作语义；（b）陈述并证明程序正确性相关的性质。该框架基于多类混合模态逻辑系统，我们为其证明了完备性结果。我们认为，我们的程序验证方法相较于模态逻辑内的现有方法有所改进，原因在于：（1）它基于操作语义，能够比动态逻辑中使用的霍尔风格最弱前置条件更自然地描述程序执行过程；（2）作为多类系统，它能够更清晰地编码语义，其表示形式与预期含义之间的表示距离更小。