Verificación formal
De Wikipedia, la enciclopedia libre
La verificación formal es un método de validación estática (se valida a través del propio código del programa), en el cual a través de especificaciones precondición/postcondición y usando la lógica de primer orden, se puede <<demostrar>> la corrección de un programa.
[editar] Precondiciones y Postcondiciones. Notación de Hoare
Una precondición es un aserto (o predicado), que se debe cumplir al comienzo de la ejecución del programa o fragmento de este. Así mismo se denomina postcondición a un aserto que se ha de cumplir tras la ejecución del programa o fragmento. Habitualmente, se utiliza la notación de Hoare, en la que se separan los asertos del pseudocódigo ( ya que, pudiera confundirse la igualdad con asignación, y es imposible demostrar mediante lógica una sentencia del tipo x = x + 1 ).
Ejemplo:
P = { n > 0 } /*predicado que actúa como precondición*/
n <- n + 1;
Q = { n > 1 } /*predicado que actúa como postcondición */
[editar] Reglas de consecuencia
Habitualmente se suele escribir un fragmento de código con la forma {P} S {Q}, donde P es un predicado que actúa como precondición, S son sentencias de cualquier tipo y Q es otro predicado que actúa como postcondición.
La 1º regla de consecuencia puede enunciarse como:
"Si existe un cierto predicado R y, {R}
{P}entonces:
{R} S {Q}"
Así mismo, el enuncidao de la 2º Regla de consecuencia es:
"Si {Q}{T}, entonces:
{P} S {T}"
El contenido de esta página es un esbozo sobre programación. Ampliándolo ayudarás a mejorar Wikipedia.
Puedes ayudarte con las wikipedias en otras lenguas.
