Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics

Andrei-Sebastian Buruiană
(Alexandru Ioan Cuza University and Bitdefender)
Ştefan Ciobâcă
(Alexandru Ioan Cuza University)

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 an expression whose value 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.

In Joachim Niehren and David Sabel: Proceedings Fifth International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2018), Oxford, England, 8th July 2018, Electronic Proceedings in Theoretical Computer Science 289, pp. 1–16.
Published: 22nd February 2019.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: