On the Generation of Equational Dynamic Logics for Weighted Imperative Programs

摘要

Dynamic logic is a powerful framework for reasoning about imperative programs. This paper extends previous work [9] on the systematic generation of dynamic logics from the propositional to the equational case, to capture 'full-fledged' imperative programs. The generation process is parametric on a structure specifying a notion of 'weight' assigned to programs. The paper introduces also a notion of bisimilar-ity on models of the generated logics, which is shown to entail modal equivalence with respect to the latter.