Geração parcial de código Java a partir de especificações formais Z (2008)
- Authors:
- Autor USP: MIYAZAWA, ALVARO HEIJI - IME
- Unidade: IME
- Sigla do Departamento: MAC
- Subjects: TÉCNICAS DE PROGRAMAÇÃO; TRANSFORMAÇÃO DE PROGRAMAS
- Agências de fomento:
- Language: Português
- Abstract: Especificações formais são úteis para descrever o que um sistema deve fazer sem definir como, e, em virtude da sua natureza formal e da possibilidade de abstração, é possível analisá-las sistematicamente. No entanto, o uso de especificações formais como parte do desenvolvimento de software não constitui prática comum. Isso se dá, em parte, pelo fato de existirem apenas um pequeno número de metodologias e ferramentas adequadas que dêem suporte a esse desenvolvimento. O primeiro objetivo deste trabalho é propor uma metodologia de desenvolvimento que possibilite, a partir de uma especificação formal em notação Z, produzir uma implementação dessa especificação em Java. Essa metodologia centra-se na geração do esqueleto da aplicação Java e na instrumentação desse esqueleto com mecanismos de verificação de condições (invariantes, pré e pós-condições) e rastreamento de violações dessas condições. Através desses mecanismos, possibilita-se intercalar desenvolvimento formal e informal no processo global de desenvolvimento de software. O segundo objetivo é desenvolver uma ferramenta que implemente parte dessa metodologia, produzindo uma implementação parcial que deverá ser complementada pelo usuário
- Imprenta:
- Data da defesa: 03.10.2008
-
ABNT
MIYAZAWA, Alvaro Heiji. Geração parcial de código Java a partir de especificações formais Z. 2008. Dissertação (Mestrado) – Universidade de São Paulo, São Paulo, 2008. Disponível em: http://www.teses.usp.br/teses/disponiveis/45/45134/tde-02112008-224245/. Acesso em: 23 abr. 2024. -
APA
Miyazawa, A. H. (2008). Geração parcial de código Java a partir de especificações formais Z (Dissertação (Mestrado). Universidade de São Paulo, São Paulo. Recuperado de http://www.teses.usp.br/teses/disponiveis/45/45134/tde-02112008-224245/ -
NLM
Miyazawa AH. Geração parcial de código Java a partir de especificações formais Z [Internet]. 2008 ;[citado 2024 abr. 23 ] Available from: http://www.teses.usp.br/teses/disponiveis/45/45134/tde-02112008-224245/ -
Vancouver
Miyazawa AH. Geração parcial de código Java a partir de especificações formais Z [Internet]. 2008 ;[citado 2024 abr. 23 ] Available from: http://www.teses.usp.br/teses/disponiveis/45/45134/tde-02112008-224245/
How to cite
A citação é gerada automaticamente e pode não estar totalmente de acordo com as normas
