especificação formal

Uma especificação formal é uma descrição matemática de software ou de hardware que pode ser utilizada para desenvolver uma implementação dos mesmos. Descreve o que sistema deve fazer, e não (necessariamente) como o deve fazer. Dada uma especificação, é possível utilizar técnicas de verificação formal para demonstrar que o modelo de um sistema candidato está de acordo com a sua especificação. Isto tem a enorme vantagem de que sistemas candidatos incorrectos são detectados e podem ser revistos antes de se investir na sua implementação. Uma aproximação alternativa é utilizar passos de refinamento para transformar uma especificação num modelo completo, e por fim numa implementação concreta. É importante notar que um modelo (ou implementação) nunca pode ser declarado «correcto» isoladamente, mas apenas «correcto no que diz respeito à sua especificação». Determinar se uma especificação formal descreve correctamente o problema a resolver, é um problema à parte. É também um problema de difícil resolução, uma vez que consiste em construir uma representação formal abstracta de um domínio de problema informal e concreto, e este passo de abstracção não é responsável nem suficiente para ser por si só uma prova formal. No entanto, é possível validar uma especificação provando teoremas relativos às propriedades que o sistema deve possuir. Se se verificarem correctos, estes teoremas reforçam a compreensão da especificação, e a sua relação com o domínio do problema. Se não, a especificação provavelmente necessita de ser alterada para melhor reflectir a compreensão do domínio de quem está envolvido na produção (e implementação) da especificação.