Um Estudo de Caso Real em Refinamento de Especificações Formais Orientadas a Objetos
Resumo
Este trabalho apresenta um método de refinamento para especificações em MooZ através de sua aplicação a um estudo de caso. MooZ é uma linguagem de especificação que é uma extensão orientada a objetos de Z. O código final obtido como produto do refinamento utiliza Eiffel, uma linguagem de programação orientada a objetos.
Palavras-chave:
Engenharia de Software, Métodos Formais, Desenvolvimento de Sistemas, Refinamento, Cálculo de Refinamento
Referências
Virgínia Adélia de Oliveira Cordeiro. De MooZ para Eiffel - Uma Abordagem Rigorosa para o Desenvolvimento de Sistemas. Tese de Mestrado, Universidade Federal de Pernambuco, Departamento de Informática, março 1994.
Virgínia A. O. Cordeiro, Augusto Sampaio, e Silvio L. Meira. De MooZ para Eiffel. Em XXI SEMISH. Caxambu. MG, agosto 1994.
Virgínia A. O. Cordeiro, Augusto Sampaio, e Silvio L. Meira. From MooZ to Eiffel - A Rigorous Approach to System Development. Em Formal Methods Europe, Barcelona. outubro 1994. A ser publicado em LNCS, Springer-Verlag, Heidelberg, DE.
S. King. Z and the Refinement Calculus. Relatório Técnico PRG-79, Oxford University Computing Laboratory, Programming Researh Group, fevereiro 1990.
S. R. L. Meira e A. L. C. Cavalcanti. Modular Object-Oriented Z Specifications. Em. Prof. C. J. van Rijsbergen, editor. Workshop on Computing Series, páginas 173 - 192, Oxford - UK, dezembro 1990. Springer-Verlag.
Bertrand Meyer. EIFFEL : The Language. Object-Oriented Series. Prentice Hall, 1992.
Caroll Morgan. Programming From Specifications. Prentice-Hall. 1990.
J. M. Spivey. The Z Notation: A Reference Manual. Prentice hall, C.A.R. Hoare Series Editor, 1989.
J.C.P. Woodcock. Mathematics as a Management Tool: Proof Rules for Promotion. Em B. A. Kitchenham, editor, Software Engineering for Large Software Systems. Elsevier Applied Science, 1990.
J. C. P. Woodcock. Implementing Promoted Operations in Z. Em C. B. Jones, R. C. Shaw, e T. Denvir, editores, Sth Refinement Workshop. BCS/Springer-Verlag Workshops in Computing, 1992.
J. C. P. Woodcock. Using Standard Z: Specification, Refinement & Proof. Book to be published, janeiro 1993.
J. B. Wordsworth. Software Development with Z: a Practical Approach to Formal Methods in Software Engineering. Addison-Wesley, 1992.
Virgínia A. O. Cordeiro, Augusto Sampaio, e Silvio L. Meira. De MooZ para Eiffel. Em XXI SEMISH. Caxambu. MG, agosto 1994.
Virgínia A. O. Cordeiro, Augusto Sampaio, e Silvio L. Meira. From MooZ to Eiffel - A Rigorous Approach to System Development. Em Formal Methods Europe, Barcelona. outubro 1994. A ser publicado em LNCS, Springer-Verlag, Heidelberg, DE.
S. King. Z and the Refinement Calculus. Relatório Técnico PRG-79, Oxford University Computing Laboratory, Programming Researh Group, fevereiro 1990.
S. R. L. Meira e A. L. C. Cavalcanti. Modular Object-Oriented Z Specifications. Em. Prof. C. J. van Rijsbergen, editor. Workshop on Computing Series, páginas 173 - 192, Oxford - UK, dezembro 1990. Springer-Verlag.
Bertrand Meyer. EIFFEL : The Language. Object-Oriented Series. Prentice Hall, 1992.
Caroll Morgan. Programming From Specifications. Prentice-Hall. 1990.
J. M. Spivey. The Z Notation: A Reference Manual. Prentice hall, C.A.R. Hoare Series Editor, 1989.
J.C.P. Woodcock. Mathematics as a Management Tool: Proof Rules for Promotion. Em B. A. Kitchenham, editor, Software Engineering for Large Software Systems. Elsevier Applied Science, 1990.
J. C. P. Woodcock. Implementing Promoted Operations in Z. Em C. B. Jones, R. C. Shaw, e T. Denvir, editores, Sth Refinement Workshop. BCS/Springer-Verlag Workshops in Computing, 1992.
J. C. P. Woodcock. Using Standard Z: Specification, Refinement & Proof. Book to be published, janeiro 1993.
J. B. Wordsworth. Software Development with Z: a Practical Approach to Formal Methods in Software Engineering. Addison-Wesley, 1992.
Publicado
26/10/1994
Como Citar
CORDEIRO, Virgínia A. O.; SAMPAIO, Augusto; MEIRA, Silvio L..
Um Estudo de Caso Real em Refinamento de Especificações Formais Orientadas a Objetos. In: SIMPÓSIO BRASILEIRO DE ENGENHARIA DE SOFTWARE (SBES), 8. , 1994, Curitiba/PR.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
1994
.
p. 143-158.
DOI: https://doi.org/10.5753/sbes.1994.24465.
