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

## TL;DR

This paper presents a language-parametric method to automatically reduce total correctness verification to partial correctness verification using rewrite theories, demonstrated with a prototype implementation on the RMT tool.

## Contribution

It introduces a novel, language-parametric transformation that simplifies total correctness proofs by leveraging partial correctness, applicable to semantics given as rewrite theories.

## Key findings

- Prototype implementation on RMT tool successfully verified several examples.
- The approach effectively reduces total correctness to partial correctness.
- Demonstrates practical applicability of the transformation in real-world scenarios.

## 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.