The B method as an environment for the verification of eiffel programs: a case study

In this paper we present an attempt to represent Eiffel programs as B specifications. Our purpose is to use the B method as an environment for the verification of the correctness of Eiffel programs. We study the difficulties associated with the representation of object oriented features (inherent t...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Aguirre, Nazareno Matías, Oviedo, Juan
Formato: Objeto de conferencia
Lenguaje:Inglés
Publicado: 2004
Materias:
Ciencias Informáticas
Object orientation
Program Verification
B Method
ARTIFICIAL INTELLIGENCE
Intelligent agents
Acceso en línea:http://sedici.unlp.edu.ar/handle/10915/22557
Aporte de:
SEDICI (UNLP) de Universidad Nacional de La Plata
id I19-R120-10915-22557
record_format dspace
institution Universidad Nacional de La Plata
institution_str I-19
repository_str R-120
collection SEDICI (UNLP)
language Inglés
topic Ciencias Informáticas
Object orientation
Program Verification
B Method
ARTIFICIAL INTELLIGENCE
Intelligent agents
spellingShingle Ciencias Informáticas
Object orientation
Program Verification
B Method
ARTIFICIAL INTELLIGENCE
Intelligent agents
Aguirre, Nazareno Matías
Oviedo, Juan
The B method as an environment for the verification of eiffel programs: a case study
topic_facet Ciencias Informáticas
Object orientation
Program Verification
B Method
ARTIFICIAL INTELLIGENCE
Intelligent agents
description In this paper we present an attempt to represent Eiffel programs as B specifications. Our purpose is to use the B method as an environment for the verification of the correctness of Eiffel programs. We study the difficulties associated with the representation of object oriented features (inherent to Eiffel programs) in the non object oriented B language. We use an extension to B in order to represent dynamic creation and deletion of objects, and show how object interaction can be achieved by borrowing some ideas from software architectures. The paper is centred on a simple and well known case study, the tra- ditional object oriented implementation of generic lists.
format Objeto de conferencia
Objeto de conferencia
author Aguirre, Nazareno Matías
Oviedo, Juan
author_facet Aguirre, Nazareno Matías
Oviedo, Juan
author_sort Aguirre, Nazareno Matías
title The B method as an environment for the verification of eiffel programs: a case study
title_short The B method as an environment for the verification of eiffel programs: a case study
title_full The B method as an environment for the verification of eiffel programs: a case study
title_fullStr The B method as an environment for the verification of eiffel programs: a case study
title_full_unstemmed The B method as an environment for the verification of eiffel programs: a case study
title_sort b method as an environment for the verification of eiffel programs: a case study
publishDate 2004
url http://sedici.unlp.edu.ar/handle/10915/22557
work_keys_str_mv AT aguirrenazarenomatias thebmethodasanenvironmentfortheverificationofeiffelprogramsacasestudy
AT oviedojuan thebmethodasanenvironmentfortheverificationofeiffelprogramsacasestudy
AT aguirrenazarenomatias bmethodasanenvironmentfortheverificationofeiffelprogramsacasestudy
AT oviedojuan bmethodasanenvironmentfortheverificationofeiffelprogramsacasestudy
bdutipo_str Repositorios
_version_ 1764820466009112576

Ejemplares similares