Imposing assertions in Maude via program transformation
Program transformation is widely used for producing correct mutations of a given program so as to satisfy the user’s intent that can be expressed by means of some sort of specification (e.g. logical assertions, functional specifications, reference implementations, summaries, examples). This paper de...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Elsevier
2019-01-01
|
| Series: | MethodsX |
| Online Access: | http://www.sciencedirect.com/science/article/pii/S2215016119303000 |
| _version_ | 1818307904708542464 |
|---|---|
| author | María Alpuente Demis Ballis Julia Sapiña |
| author_facet | María Alpuente Demis Ballis Julia Sapiña |
| author_sort | María Alpuente |
| collection | DOAJ |
| description | Program transformation is widely used for producing correct mutations of a given program so as to satisfy the user’s intent that can be expressed by means of some sort of specification (e.g. logical assertions, functional specifications, reference implementations, summaries, examples). This paper describes an automated correction methodology for Maude programs that is based on program transformation and can be used to enforce a safety policy, given by a set A of system assertions, in a Maude program R that might disprove some of the assertions. The outcome of the technique is a safe program refinement R' of R in which every computation is a good run, i.e., it satisfies the assertions in A. Furthermore, the transformation ensures that no good run of R is removed from R'. Advantages of this correction methodology can be summarized as follows. • A fully automatic program transformation featuring both program diagnosis and repair that preserves all executability requirements. • A simple logical notation to declaratively express invariant properties and other safety constraints through assertions. • No dynamic information is required to infer program fixes: the methodology is static and does not need to collect any error symptom at runtime. Method name: Transformation method for enforcing system invariants in Maude programs, Keywords: Assertion enforcement, Automated program transformation, Program repair, Equational rewriting, Rewriting logic, Maude |
| first_indexed | 2024-12-13T07:05:48Z |
| format | Article |
| id | doaj.art-7710e061e5204c4c8933d21d48f8c34b |
| institution | Directory Open Access Journal |
| issn | 2215-0161 |
| language | English |
| last_indexed | 2024-12-13T07:05:48Z |
| publishDate | 2019-01-01 |
| publisher | Elsevier |
| record_format | Article |
| series | MethodsX |
| spelling | doaj.art-7710e061e5204c4c8933d21d48f8c34b2022-12-21T23:55:49ZengElsevierMethodsX2215-01612019-01-01625772583Imposing assertions in Maude via program transformationMaría Alpuente0Demis Ballis1Julia Sapiña2VRAIN (Valencian Research Institute for Artificial Intelligence), Universitat Politècnica de València, Camino de Vera s/n, Apdo 22012, 46071 Valencia, Spain; Corresponding author.DMIF, University of Udine, Via delle Scienze, 206, 33100 Udine, ItalyVRAIN (Valencian Research Institute for Artificial Intelligence), Universitat Politècnica de València, Camino de Vera s/n, Apdo 22012, 46071 Valencia, SpainProgram transformation is widely used for producing correct mutations of a given program so as to satisfy the user’s intent that can be expressed by means of some sort of specification (e.g. logical assertions, functional specifications, reference implementations, summaries, examples). This paper describes an automated correction methodology for Maude programs that is based on program transformation and can be used to enforce a safety policy, given by a set A of system assertions, in a Maude program R that might disprove some of the assertions. The outcome of the technique is a safe program refinement R' of R in which every computation is a good run, i.e., it satisfies the assertions in A. Furthermore, the transformation ensures that no good run of R is removed from R'. Advantages of this correction methodology can be summarized as follows. • A fully automatic program transformation featuring both program diagnosis and repair that preserves all executability requirements. • A simple logical notation to declaratively express invariant properties and other safety constraints through assertions. • No dynamic information is required to infer program fixes: the methodology is static and does not need to collect any error symptom at runtime. Method name: Transformation method for enforcing system invariants in Maude programs, Keywords: Assertion enforcement, Automated program transformation, Program repair, Equational rewriting, Rewriting logic, Maudehttp://www.sciencedirect.com/science/article/pii/S2215016119303000 |
| spellingShingle | María Alpuente Demis Ballis Julia Sapiña Imposing assertions in Maude via program transformation MethodsX |
| title | Imposing assertions in Maude via program transformation |
| title_full | Imposing assertions in Maude via program transformation |
| title_fullStr | Imposing assertions in Maude via program transformation |
| title_full_unstemmed | Imposing assertions in Maude via program transformation |
| title_short | Imposing assertions in Maude via program transformation |
| title_sort | imposing assertions in maude via program transformation |
| url | http://www.sciencedirect.com/science/article/pii/S2215016119303000 |
| work_keys_str_mv | AT mariaalpuente imposingassertionsinmaudeviaprogramtransformation AT demisballis imposingassertionsinmaudeviaprogramtransformation AT juliasapina imposingassertionsinmaudeviaprogramtransformation |