Métodos Formales de verificaciones de programas.

Aserciones7
Una parte importante de uan verificación formal es la documentación de un programa atraves de asertos o afirmaciones – sentencias logicas ciertas hacerca del programa que se declaran verdaderas-. Un aserto se escribe como un comentario y describe lo que se supone sea verdadero sobre las variables del programa en ese punto.

Precondiciones y poscondiciones
Las precondiciones y poscondiciones son afirmaciones sencillas sobre condiciones al principio y al final de los modulos.

Reglas para prueba de programas
Un medio util para probar que un programa p hace lo que realmente ha de hacer es proporcional aserciones que expresen las condiciones antes y después de que p sea ejecutado. En realidad las aserciones son como sentencias o declaraciones que pueden ser o bien verdaderas o bien falsas.

Invariantes de bucles
Una invariante de bucle es una condicion que es verdadera antes y después de la ejecución de un bucle. Las invariantes de bucle se utilizan para demostrar la conexión (exactitud) de algoritmos iterativos. Utilizando invariantes se pueden detectar errores antes de comenzar la codificacion y por esa razon reducir tiempo de depuración y prueba.