Proving Correctness of Graph Programs Relative to Recursively Nested Conditions

Nils Erik Flick


We propose a new specification language for the proof-based approach to verification of graph programs by introducing mu-conditions as an alternative to existing formalisms which can express path properties. The contributions of this paper are the lifting of constructions from nested conditions to the new, more expressive conditions and a proof calculus for partial correctness relative to mu-conditions. In particular, we exhibit and prove the correctness of a construction to compute weakest preconditions with respect to finite graph programs.

Full Text:




Hosted By Universitätsbibliothek TU Berlin.