MAC 0499 - Trabalho de Formatura SupervisionadoGeração Automática de Código a partir de Especificação Formal
Para que seja possível gerar código a partir da especificação de um software, a especificação precisa ser bem definida e não deve possuir ambiguidades. Assim, a geração de código tendo como base especificação em linguagem natural fica inviável pela própria característica da linguagem natural, a qual possui ambiguidades e é passível de múltiplas interpretações para um mesmo texto. Por esse motivo, para a geração de código a partir de especificação em UML (Unified Modeling Language), que é a maneira mais utilizada para especificar, é difícil garantir a corretude do código produzido, pois essa linguagem baseia-se em diagramas e casos de uso, em linguagem natural. Desse modo, havia a necessidade de se utilizar uma especificação formal como base para gerar o código. Após um levantamento dos trabalhos existentes em geração de código a partir de especificação formal, decidiu-se por aperfeiçoar o arcabouço feito pelo Álvaro H. Miyazawa e Paulo Salem, ampliando o uso dessa ferramenta para cobrir um maior subconjunto da notação Z. Esse arcabouço gera código fonte em linguagem de programação Java a partir de um arquivo de especificação formal em notação Z, definida pelo padrão ISO/IEC 13568, no formato LaTeX, produzida com base nos requisitos do sistema a ser implementado.
|
