Tags:operational semantics, partial correctness, program transformation, program verification, reachability logic, termination and total correctness
Abstract:
We give a language-parametric solution to the problem of total correctness, by automatically reducing it to the problem of partial correctness, under the assumption that a variant that decreases with each program step in a well-founded order is provided. Our approach assumes that the programming language semantics is given as a rewrite theory. We implement a prototype on top of the RMT tool and we show that it works in practice on a number of examples.
Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics