Una prueba de técnica de corrección en que afirmaciones están escritos describiendo condiciones intermedias, salidas y entradas de programa, se desarrolla un conjunto de teoremas relativos a satisfacción de las afirmaciones de entrada a la satisfacción de las afirmaciones de salida y los teoremas son probados o refutados utilizando prueba por inducción.