Corretude (lógica)
Este artigo não cita fontes confiáveis. (Abril de 2013) |
Na Ciência da computação teórica, a corretude de um algoritmo pode ser afirmada quando se diz que o algoritmo é correto com respeito à determinada especificação. O termo corretude funcional se refere ao comportamento de entrada-saída do algorítimo (isto é, para cada entrada ele produz a saída correta).
É feita uma distinção entre corretude total, que requer que o algoritmo tenha um fim, e corretude parcial, que requer simplesmente que se o algoritmo retornar uma resposta ela esteja correta. Uma vez que não há nenhuma solução geral para o Problema da parada, afirmar a corretude total de um algoritmo pode ser algo muito difícil. A [Análise de término] é um tipo de prova matemática que desempenha um papel muito importante na verificação formal por que a corretude total de um algoritmo depende de seu término.
Por exemplo, buscando sucessivamente através dos números inteiros 1, 2, 3, … para ver se encontramos algum tipo de fenômeno — como encontrar um número perfeito — é muito fácil escrever um programa parcialmente correto. Mas para dizer que este programa é totalmente correto seria afirmar algo ainda desconhecido na teoria dos números.
Uma prova teria de ser uma prova matemática, supondo que o algoritmo e a especificação estão dados formalmente. Em particular não se espera uma afirmação de corretude de um determinado programa implementando um algoritmo numa dada máquina. Pois envolveria algumas considerações como limitações na memória do computador.
Na teoria da prova, o Isomorfismo de Curry-Howard, afirma que uma prova da corretude funcional na Lógica intuicionista corresponde a um certo programa no Cálculo lambda. Converter uma prova dessa maneira é chamado extração de programa.
Lógica de Hoare é um Sistema formal específico com um conjunto de regras lógicas para um raciocínio rigoroso sobre a corretude na computação.