Métodos formais: diferenças entre revisões

'''Nível 2:''' [[Provadores de teoremas]] podem ser usados para conduzir testes completos das propriedades de um sistema de maneira automatizada. Este método pode se revelar muito dispendioso, sendo apenas vantajoso se o custo provocado pelos erros for extremamente alto (ep.gex., em partes críticas do projeto de um [[microprocessador]]).

* [[Operações semânticas]]: um sistema é expresso como uma seqüênciasequência de ações de um modelo computacional (presumidamente) mais simples. Defensores desse método apontam para a simplicidade dos seus modelos como meio de expressar claridade; os críticos consideram que os problemas envolvendo semântica ainda não foram resolvidos (quem define a semântica de um modelo mais simples?).

* [[Axiomatizações semânticas]]: um sistema é expresso em termos de [[pré-condições]] e [[pós-condições]] que são verdadeiras antes e depois do sistema executar uma tarefa, respectivamenterespetivamente. Defensores apontam a conexão com a [[lógica clássica]]; os críticos dizem que tais semânticas nunca descrevem de fato o que um sistema ''faz'' (meramente o que é verdade antes e depois).

Às vezes, a motivação para provar a correção de um sistema não é a necessidade óbvia de reassegurar a correção do sistema, mas um desejo de entender melhor o sistema. ConseqüentementeConsequentemente, algumas provas de correção são produzidas no estilo de [[prova matemática]]: manuscritas (ou digitadas) usando [[linguagem natural]], em um nível de informalidade comum a provas dessa categoria. Uma “boa” prova é uma que seja legível e inteligível por outros leitores humanos.

Críticos dessa abordagem afirmam que a [[ambigüidadeambiguidade]] inerente da linguagem natural leva a erros indetectáveisindetetáveis; freqüentementefrequentemente, erros sutis podem estar presentes em detalhes de baixo nível tipicamente negligenciados por essas provas. Adicionalmente, o trabalho envolvido em produzir uma boa prova requer um alto nível de sofisticação e especialização matemática.

O campo dos métodos formais tem seus críticos. Provas de correção, manuscritas ou assistidas por computador, precisam de tempo significante (e, portanto, de dinheiro) para serem produzidas, com utilidade limitada e voltadas apenas para assegurar a precisão. Por essa razão, os métodos formais são mais frequentemente usados em áreas onde os benefícios de se conseguir essas provas, ou o risco de haver erros não detectadosdetetados, compensam os recursos empregados. Exemplo: na [[engenharia aeroespacial]], erros não detectadosdetetados podem causar [[mortes]], portanto métodos formais são mais populares nesta área em comparação a outras.