Alpuente Frasnedo, M.; Ballis, D.; Sapiña Sanchis, J. (2018). Static Correction of Maude Programs with Assertions. http://hdl.handle.net/10251/100268
Por favor, use este identificador para citar o enlazar este ítem: http://hdl.handle.net/10251/100268
Title:
|
Static Correction of Maude Programs with Assertions
|
Author:
|
Alpuente Frasnedo, María
Ballis, D.
Sapiña Sanchis, Julia
|
UPV Unit:
|
Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació
|
Issued date:
|
|
Abstract:
|
In this paper, we present a novel transformation method for Maude programs featuring both automatic program diagnosis and correction. The input of our method is a reference specification A of the program behavior that ...[+]
In this paper, we present a novel transformation method for Maude programs featuring both automatic program diagnosis and correction. The input of our method is a reference specification A of the program behavior that is given in the form of assertions together with an overly general program R whose execution might violate the assertions. Our technique translates R into a refined program R' in which every computation is a computation in R that satisfies the assertions of A.
Our correction technique is first formalized for topmost rewrite theories, and then we generalize it to larger rewrite theories that support nested structured configurations.
Our technique copes with infinite space states and does not require the knowledge of any failing run. We report experiments that assess the effectiveness of assertion-driven correction.
[-]
|
Subjects:
|
Asertion checking
,
Program repair
,
Program transformation
,
Rewriting logic
,
Equational rewriting
,
Maude
|
Copyrigths:
|
Reserva de todos los derechos
|
Publisher:
|
Universitat Politècnica de València
|
Project ID:
|
MINECO/TIN2015-69175-C4-1-R
GVA/PROMETEOII/2015/013
|
Thanks:
|
This work has been partially supported by the EU (FEDER) and the Spanish MINECO under grants TIN2015-69175-C4-1-R, and by Generalitat Valenciana ref. PROMETEOII/2015/013
|
Type:
|
Informe
|