Dynamic logic and its variations, because of their clear and expressive forms for capturing program properties, have been used as formalisms in program/system specification and verification for years and have many other applications. The program models of dynamic logics are in explicit forms. For different target program models, different dynamic logic theories have to be proposed to adapt different models' semantics. In this paper, we propose a parameterized `dynamic-logic-style' formalism, namely $DL_p$, for specifying and reasoning about general program models. In $DL_p$, program models and logical formulas are taken as `parameters', allowing arbitrary forms according to different interested domains. This characteristic allows $DL_p$ to support direct reasoning based on the operational semantics of program models, while still preserving compositional reasoning based on syntactic structures. $DL_p$ provides a flexible verification framework to encompass different dynamic logic theories. In addition, it also facilitates reasoning about program models whose semantics is not compositional, examples are neural networks, automata-based models, synchronous programming languages, etc. We mainly focus on building the theory of $DL_p$, including defining its syntax and semantics, building a proof system and constructing a cyclic preproof structure. We analyze and prove the soundness of $DL_p$. Case studies show how $DL_p$ works for reasoning about different types of program models.

翻译：动态逻辑及其变体因其清晰且富有表现力的程序属性刻画形式，多年来一直被用作程序/系统规约与验证的形式化工具，并拥有众多其他应用。动态逻辑的程序模型采用显式形式。针对不同的目标程序模型，必须提出不同的动态逻辑理论以适应不同模型的语义。本文提出一种参数化的“动态逻辑风格”形式化方法，即$DL_p$，用于规约和推理通用程序模型。在$DL_p$中，程序模型和逻辑公式被视为“参数”，可根据不同关注领域采用任意形式。这一特性使得$DL_p$能够支持基于程序模型操作语义的直接推理，同时仍保留基于语法结构的组合式推理。$DL_p$提供了一个灵活的验证框架，可涵盖不同的动态逻辑理论。此外，它还促进了语义非组合性程序模型的推理，例如神经网络、基于自动机的模型、同步编程语言等。我们主要致力于构建$DL_p$的理论体系，包括定义其语法与语义、构建证明系统以及构造循环预证明结构。我们分析并证明了$DL_p$的可靠性。案例研究展示了$DL_p$如何用于不同类型程序模型的推理。