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...
Main Authors: | , |
---|---|
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 |