Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics
Logic in Computer Science
2019-02-25 v1 Programming Languages
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 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.
Cite
@article{arxiv.1902.08419,
title = {Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics},
author = {Andrei-Sebastian Buruiană and Ştefan Ciobâcă},
journal= {arXiv preprint arXiv:1902.08419},
year = {2019}
}
Comments
In Proceedings WPTE 2018, arXiv:1902.07818