Verification of graph programs with monadic second-order logic

In this thesis, we consider Hoare-style verification for the graph programming language GP 2. In literature, Hoare-style verification for graph programs has been studied by using extensions of nested conditions called E-conditions and M-conditions as assertions. However, E-conditions are only able to express first-order properties of GP 2 graphs, while M-conditions can only express properties of a non-attributed graph. Hence, there is still no logic that can express monadic second-order properties of GP 2 graphs. Moreover, both E-conditions and M-conditions may not be easy to comprehend by programmers used to formal specifications expressed in standard first-order logic.

Here, we present an approach to verify GP 2 graph programs with a standard monadic second-order logic. We show how to construct a strongest liberal postcondition with respect to a rule schema and a precondition. We then extend this construction to obtain a strongest liberal postcondition for arbitrary loop-free programs. Also, we show how to construct a precondition expressing successful execution of a loop-free program, and failing execution of a so-called iteration command. These constructions allow us to define a partial proof calculus that can handle a larger class of graph programs than what can be verified by the calculus that uses E-conditions and M-conditions as assertions.

Other than partial proof calculus whose assertions are monadic second-order logic, we also define semantic partial proof calculus. Similar calculus has been introduced in literature, but here we update the calculus by considering a GP 2 command that was not considered in existing work.