Métodos Formais na Especificação de Interfaces com o Utilizador: a Linguagem VDM++ e o Tratamento de Eventos

Resumo

Este artigo faz uma avaliação da utilização de uma linguagem geral de especificação, VDM++, para especificação de interfaces com o utilizador analisando em particular uma das suas limitações que condicionam a sua aplicabilidade (o tratamento de eventos). Começa por uma classificação geral dos Métodos Formais existentes de acordo com os aspectos em que se baseiam (modelos, propriedades ou comportamentos) referindo as diferentes abordagens de aplicação destes métodos à especificação de interfaces. De seguida, é apresentado o caso de estudo onde se cria uma especificação, em VDM++, para um diálogo (validação de um utilizador e a sua palavra-chave) por um processo de engenharia reversa do código C# necessário para a implementação desse diálogo, avaliando-se a utilização da linguagem e apresentando-se uma solução para o tratamento de eventos.