Método formal

En 1976, Edsger Dijkstra, presentó un método formal llamado precondición más débil, basado en la transformación de predicados wp (weakest precondition).Se garantiza que si la entrada actual satisface las restricciones de entrada (precondiciones) la salida satisface las restricciones de salida (poscondiciones).Este método permite tanto la corrección parcial como total de los programas.Un caso especial son los bucles, donde los predicados deben mostrar una relación invariante, es decir, deben ser ciertos independientemente del número de vueltas del bucle, por lo tanto el predicado debe cumplir lo siguiente: Básicamente, consiste en dada una poscondición POST, encontrar, operando hacia atrás, un programa S tal que wp(S, POST) (la precondición) se satisfaga en un amplio conjunto de situaciones Dada una proposición (P) S (Q) donde S es un conjunto de sentencias de un módulo de un programa, y donde P y Q son los predicados que se cumplen antes y después de S respectivamente, se dice que P es la precondición más débil (wp) de S, si es la condición mínima que garantiza que Q es cierto tras la ejecución de S. La inducción estructural es una técnica de verificación formal que se basa en el principio de inducción matemática.Dado un conjunto S con una serie de propiedades y una proposición P que se desea probar, la inducción matemática: La clasificación más común se realiza en base al modelo matemático subyacente en cada método, de esta manera podrían clasificarse en: