Correção

Prévia do material em texto

Correção 
Na ciência da computação teórica, a correção de um algoritmo é afirmada 
quando se diz que o algoritmo está correto em relação a uma especificação. 
A correção funcional se refere ao comportamento de entrada-saída do 
algoritmo (ou seja, para cada entrada, ele produz a saída esperada). 
É feita uma distinção entre correção parcial, que requer que se uma resposta 
for retornada, ela será correta, e correção total, que adicionalmente requer 
que o algoritmo seja encerrado. Visto que não há solução geral para o 
problema da parada, a correção total não é decidível. Uma prova de 
terminação é um tipo de prova matemática que desempenha um papel crítico 
na verificação formal porque a correção total de um algoritmo depende da 
terminação. 
 
Por exemplo, procurando sucessivamente por inteiros 1, 2, 3,.. para ver se 
podemos encontrar um exemplo de algum fenômeno - digamos um número 
perfeito ímpar - é bastante fácil escrever um programa parcialmente correto 
(usando fatoração para calcular a alíquota de cada inteiro soma ). Mas dizer 
que este programa é totalmente correto seria afirmar algo atualmente 
desconhecido na teoria dos números. 
Uma prova teria que ser uma prova matemática, assumindo que tanto o 
algoritmo quanto a especificação são dados formalmente. Em particular, não 
se espera que seja uma afirmação de correção para um determinado 
programa que implementa o algoritmo em uma determinada máquina. Isso 
envolveria considerações como limitações na memória do computador. 
Um resultado profundo na teoria da prova, a correspondência Curry-Howard, 
afirma que uma prova de correção funcional na lógica construtiva 
corresponde a um certo programa no cálculo lambda. A conversão de uma 
prova dessa maneira é chamada de extração de programa. 
A lógica Hoare é um sistema formal específico para raciocinar rigorosamente 
sobre a correção dos programas de computador. Ele usa técnicas axiomáticas 
para definir a semântica da linguagem de programação e argumentar sobre a 
correção de programas por meio de afirmações conhecidas como triplas de 
Hoare. 
Teste de software é qualquer atividade destinada a avaliar um atributo ou 
capacidade de um programa ou sistema e determinar se ele atende aos 
resultados exigidos. Embora crucial para a qualidade do software e 
amplamente implementado por programadores e testadores, o teste de 
software ainda permanece uma arte, devido à compreensão limitada dos 
princípios do software. A dificuldade em testar software decorre da 
complexidade do software: não podemos testar completamente um programa 
com complexidade moderada. 
O teste é mais do que apenas depurar. O objetivo do teste pode ser garantia 
de qualidade, verificação e validação ou estimativa de confiabilidade. O teste 
também pode ser usado como uma métrica genérica. Teste de exatidão e teste 
de confiabilidade são duas áreas principais de teste. O teste de software é 
uma compensação entre orçamento, tempo e qualidade.