Introdução a Linguagem Z

Métodos Formais com Linguagem Z: Uma Introdução

Resumo. O presente trabalho busca a apresentação da utilização de especificação formal de software com a linguagem formal Z, trazendo suas características principais e exemplificando através do uso de um Software de Help Desk.
1. Introdução
Foi buscando a minimização de falhas que os softwares passaram por diversas mudanças nos processos de engenharia e as linguagens de programação evoluíram para evitar a ocorrência de instabilidades nos sistemas por elas desenvolvidos, utilizando conceitos como rigidez de tipos, tratamento de exceções, verificação em tempo de compilação, etc. Linguagens modernas como Java, Python, C# e tantas outras trazem consigo ideias baseadas nestes conceitos. Neste contexto, a Linguagem Z surgiu também para o uso no tratamento de erros, estes presentes em sistemas caso sejam produzidos sem uma especificação de requisitos robusta.
2. Especificação Formal
Ao caracterizar uma falha em sistemas computacionais é preciso ter em mente o processo de fabricação de software e o ambiente que descreve tal ambiente. As falhas podem ser divididas entre: Falha de sistema, de Hardware, de Software e humanas. Sendo que delas, apenas a falha de Hardware é a mais complicada de se tratar na hora de se construir um software, tendo em vista que a especificação formal poderá atenuar estas falhas de sistema e software e uma boa documentação pode minimizar uma falha dita humana.
Alguns testes podem ser efetuados na busca por falhas, entre eles podemos destacar os testes experimentais e os exaustivos – sendo este o que mais garante a ausência de falhas, porém sua usabilidade é impraticável, por gerar um trabalho excessivo e demasiado demorado para o teste.
Aqui se deparamos como os métodos formais como forma de assumir uma menor incidência de falhas no desenvolvimento de software, por meio de técnicas que levam em conta requisitos, modelos, programas e transformações formais. Estas transformações utilizam