Specification Slicing for VDM-SL
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866913530753581056 |
|---|---|
| author | Oda, Tomohiro Chang, Han-Myung |
| author_facet | Oda, Tomohiro Chang, Han-Myung |
| contents | The executable specification is one of the powerful tools in lightweight formal software development. VDM-SL allows the explicit and executable definition of operations that reference and update internal state through imperative statements. While the extensive executable subset of VDM-SL enables validation and testing in the specification phase, it also brings difficulties in reading and debugging as in imperative programming. In this paper, we define specification slicing for VDM-SL based on program slicing, a technique used for debugging and maintaining program source code in implementation languages. We then present and discuss its applications. The slicer for VDM-SL is implemented on ViennaTalk and can be used on browsers and debuggers describing the VDM-SL specification. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_03180 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Specification Slicing for VDM-SL Oda, Tomohiro Chang, Han-Myung Software Engineering The executable specification is one of the powerful tools in lightweight formal software development. VDM-SL allows the explicit and executable definition of operations that reference and update internal state through imperative statements. While the extensive executable subset of VDM-SL enables validation and testing in the specification phase, it also brings difficulties in reading and debugging as in imperative programming. In this paper, we define specification slicing for VDM-SL based on program slicing, a technique used for debugging and maintaining program source code in implementation languages. We then present and discuss its applications. The slicer for VDM-SL is implemented on ViennaTalk and can be used on browsers and debuggers describing the VDM-SL specification. |
| title | Specification Slicing for VDM-SL |
| topic | Software Engineering |
| url | https://arxiv.org/abs/2410.03180 |