Applying dynamic logics to program verifications is a challenge, because their axiomatic rules for regular expressions can be difficult to be adapted to different program models. We present a novel dynamic logic, called DLp, which supports reasoning based on programs' operational semantics. For those programs whose transitional behaviours are their standard or natural semantics, DLp makes their verifications easier since one can directly apply the program transitions for reasoning, without the need of re-designing and validating new rules as in most other dynamic logics. DLp is parametric. It provides a model-independent framework consisting of a relatively small set of inference rules, which depends on a given set of trustworthy rules for the operational semantics. These features of DLp let multiple models easily compared in its framework and makes it compatible with existing dynamic-logic theories. DLp supports cyclic reasoning, providing an incremental derivation process for recursive programs, making it more convenient to reason about without prior program transformations. We analyze and prove the soundness and completeness of DLp under certain conditions. Several case studies illustrate the features of DLp and fully demonstrate its potential usage.

翻译：将动态逻辑应用于程序验证是一项挑战，因为其正则表达式的公理化规则难以适配不同的程序模型。我们提出了一种新颖的动态逻辑，称为DLp，它支持基于程序操作语义的推理。对于那些以转换行为作为其标准或自然语义的程序，DLp使得它们的验证更为容易，因为人们可以直接应用程序转换进行推理，而无需像大多数其他动态逻辑那样重新设计和验证新规则。DLp是参数化的。它提供了一个模型无关的框架，包含一组相对较少的推理规则，这些规则依赖于给定的一组关于操作语义的可信规则。DLp的这些特性使得多种模型能够在其框架内轻松比较，并使其与现有的动态逻辑理论兼容。DLp支持循环推理，为递归程序提供了增量推导过程，使得无需预先进行程序变换即可更方便地进行推理。我们分析并证明了DLp在特定条件下的可靠性和完备性。若干案例研究展示了DLp的特性，并充分证明了其潜在用途。