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 correction technique translates R into a refined program R' in which every computation is also a computation in R that satisfies the assertions of A. The technique is first formalized for topmost rewrite theories, and then we generalize it to larger classes of 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.

Static correction of Maude programs with assertions

Ballis, D.;
2019

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 is given in the form of assertions together with an overly general program R whose execution might violate the assertions. Our correction technique translates R into a refined program R' in which every computation is also a computation in R that satisfies the assertions of A. The technique is first formalized for topmost rewrite theories, and then we generalize it to larger classes of 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.
File in questo prodotto:
File Dimensione Formato  
jss-2019.pdf

non disponibili

Tipologia: Versione Editoriale (PDF)
Licenza: Non pubblico
Dimensione 1.36 MB
Formato Adobe PDF
1.36 MB Adobe PDF   Visualizza/Apri   Richiedi una copia
JSS2manuscript.pdf

accesso aperto

Tipologia: Documento in Pre-print
Licenza: Creative commons
Dimensione 841.16 kB
Formato Adobe PDF
841.16 kB Adobe PDF Visualizza/Apri
JSS3-postprint.pdf

embargo fino al 26/03/2021

Tipologia: Documento in Post-print
Licenza: Creative commons
Dimensione 874.88 kB
Formato Adobe PDF
874.88 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11390/1148107
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 4
  • ???jsp.display-item.citation.isi??? 4
social impact