Condición de verificación

Definición

Una condición de verificación (VC) es una fórmula lógica cuya validez basta para justificar un paso de la prueba de un programa anotado. El generador de VCs elimina los comandos y deja obligaciones de lógica o aritmética.

Proceso

1. Una persona anota el programa con condiciones intermedias e invariantes.
2. Un generador produce VCs mecánicamente.
3. Un demostrador automático o una persona prueba cada VC.

Para una asignación:

$$\{P\}V:=E\{Q\}$$

genera:

$$P\Rightarrow Q_E^V,\text{donde }{Q}_E^V\equiv Q[E/V].$$

Para un ciclo anotado:

{P} while B do {I} C {Q}

genera al menos:

$$P\Rightarrow I,$$ $$I\wedge \neg B\Rightarrow Q,$$

y las VCs de:

$$\{I\wedge B\}C\{I\}.$$

Ejemplo mínimo

Para

$$\{x=0\}x:=x+1\{x=1\},$$

la VC es:

$$x=0\Rightarrow x+1=1,$$

que es válida.

Límites

El generador puede ser mecánico, pero elegir un invariante útil normalmente requiere entender el algoritmo. Si las anotaciones son demasiado débiles, las VCs no permiten llegar a la postcondición; si son incorrectas, alguna VC falla.

Relaciones

• Formaliza pruebas de: ternas de Hoare.
• Usa: sustitución, ramas e invariantes.
• Para corrección total agrega una: función variante.

Procedencia

• Fuente: /Users/diegovillalba/Downloads/AllLectures.pdf, páginas PDF 47–69.
• Desarrollo guiado: De programa anotado a condiciones de verificación.