Proving Correctness of Graph Programs Relative to Recursively Nested Conditions
Nils Erik Flick · Carl von Ossiezky University of Oldenburg · 2016
With graph programs, one can formally model the behaviour of a wide range of discrete systems. These programs extend graph rewriting by control structures (sequence, choice and iteration). This thesis presents a theoretically founded formalism for specifying properties of graph programs and a proof-based approach to verifying the partial correctness of a graph program relative to a pre- and postcondition. A novel specification language, recursively nested conditions (mu-conditions) is introduced, which can express nonlocal state properties and which is shown to be distinct from other relevant formalisms. The verification approach consists of: an adaptation of Dijkstra's weakest precondition calculus to graph programs and mu-conditions, a proof calculus for mu-conditions, whose core part is a rule schema for inductive refutation. Additionally, a formulation of correctness under adversity and structure-changing Petri nets are elaborated within the same framework.