On A Parameterized Theory of Dynamic Logic for Operationally-based Programs

TL;DR

This paper introduces DLp, a parameterized dynamic logic that simplifies reasoning about operational semantics of programs, especially recursive ones, by providing a flexible, model-independent framework with soundness and completeness proofs.

Contribution

DLp is a novel, parametric dynamic logic that supports reasoning directly from operational semantics, enabling easier verification of recursive and cyclic programs without redesigning rules.

Findings

DLp facilitates direct reasoning from operational semantics.

It supports cyclic reasoning for recursive programs.

DLp is proven sound and complete under certain conditions.

Abstract

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.