Métodos Formales de verificaciones de programas.

Aunque la verificacion formal se sale fuera del ambito, por su importancia se van a tomar dos conceptos clave, asertos (afirmaciones) y precondiciones/postcondiciones invariantes que ayudan a documentar, corregir y clarificar el diseño de modulos y de programas.

Aserciones
Una parte importante de una verificacion formal es la documentacion de un programa a traves de asertos o afirmaciones-sentencias logicas acerca del programa que se declaran <>-. Un aserto se escribe como un comentario y describe lo que se supone sea verdadero sobre las variables del programa en ese punto.
Un aserto es una frase sobre una condicion especifica en un cierto punto de un algoritmo o programa.

Precondiciones y postcondiciones
Son afirmaciones sencillas sobre condiciones al principio y al final de los modulos. Una precondicion de un procedimiento es una afirmacion logica sobre sus parametros de entrada; se supone que es verdadera cuando se llama al procedimiento. una postcondicion de un procedimiento puede ser una afirmacion logica que describe el cambio en el estado del programa producido por la ejecucion del procedimiento; la postcondicion describe el efecto de llamar al procedimiento. En otras palabras, la postcondicion indica que sera verdadera despues de que se ejecute el procedimiento.