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）作为多类系统，它能更清晰地编码语义，与其预期含义之间的表示距离更小。