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}"