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

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

Full description

Bibliographic Details
Main Authors: Andrei-Sebastian Buruiană, Ştefan Ciobâcă
Format: Article
Language:English
Published: Open Publishing Association 2019-02-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1902.08419v1
_version_ 1818991000169742336
author Andrei-Sebastian Buruiană
Ştefan Ciobâcă
author_facet Andrei-Sebastian Buruiană
Ştefan Ciobâcă
author_sort Andrei-Sebastian Buruiană
collection DOAJ
description 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.
first_indexed 2024-12-20T20:03:18Z
format Article
id doaj.art-73ff740ab2f94987b93d75e7897c5b1c
institution Directory Open Access Journal
issn 2075-2180
language English
last_indexed 2024-12-20T20:03:18Z
publishDate 2019-02-01
publisher Open Publishing Association
record_format Article
series Electronic Proceedings in Theoretical Computer Science
spelling doaj.art-73ff740ab2f94987b93d75e7897c5b1c2022-12-21T19:28:00ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802019-02-01289Proc. WPTE 201811610.4204/EPTCS.289.1:5Reducing Total Correctness to Partial Correctness by a Transformation of the Language SemanticsAndrei-Sebastian Buruiană0Ştefan Ciobâcă1 Alexandru Ioan Cuza University and Bitdefender 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.http://arxiv.org/pdf/1902.08419v1
spellingShingle Andrei-Sebastian Buruiană
Ştefan Ciobâcă
Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics
Electronic Proceedings in Theoretical Computer Science
title Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics
title_full Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics
title_fullStr Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics
title_full_unstemmed Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics
title_short Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics
title_sort reducing total correctness to partial correctness by a transformation of the language semantics
url http://arxiv.org/pdf/1902.08419v1
work_keys_str_mv AT andreisebastianburuiana reducingtotalcorrectnesstopartialcorrectnessbyatransformationofthelanguagesemantics
AT stefanciobaca reducingtotalcorrectnesstopartialcorrectnessbyatransformationofthelanguagesemantics