VDM-TXT: Um Tradutor de Especificação em VDM para Linguagem Natural

Um dos principais problemas do desenvolvimento de sistemas é a existência de erros no software recém criado. Testes não resolvem este problema, pois nunca são completos e só servem para mostrar a existência de erros, e não a sua ausência.

O uso de métodos formais de especificação permite a verificação matemática da correção de um sistema, porém usuários finais não têm preparo para ler e validar estas especificações.

O VDM-TXT gera um texto em linguagem natural a partir de uma especificação formal, de tal forma que usuários possam validar o entendimento do analista de sistemas a respeito do problema a ser resolvido.