Arte

PROGRAMACIÓN PROCEDURAL

Verificación y Derivación formal de Programas

1

Enfoques para determinar si un programa es correcto
validar

Testing:
Sólo puede mostrar la presencia de errores y no su inexistencia.
Para asegurar que un programa es correcto es necesario analizar todos los
valores posibles de datos de entrada (imposible cuando el cjto. es infinito)

Prueba formal deprogramas:
.
Asegura que el programa es correcto con respecto a una especificación para todas
las entradas

Dos problemas importantes:
1) la manipulación lógica puede ser tediosa y propensa a errores;
2) la prueba solamente muestra que el programa implementa la
especificación correctamente. No hay certeza de que la especificación
describe lo que el usuario realmente desea

VerificaciónFormal
Para la verificación de programas Imperativos se utiliza un sistema de reglas basado
en la tripla de Hoare

Tripla de Hoare

{ P} A {Q}

A : programa/ sentencia;
P y Q predicados o aserciones

Interpretación :Si el predicado P es cierto antes de la ejecución del programa A y el
programa termina , entonces Q será cierto tras la ejecución de A.

La precondición P y la postcondiciónQ se especifican mediante fórmulas denominadas
aserciones. Se garantiza que si la entrada actual satisface las restricciones de entrada
(precondiciones) la salida satisface las restricciones de salida (postcondiciones)

Precondiciones y Postcondiciones
{ P} A {Q}
El programa A actúa como una función de estados en estados: comienza su
ejecución en un estado inicial válido, descrito por elvalor de los parámetros de
entrada, y termina en un estado final en el que los parámetros de salida contienen

los resultados esperados.
 Espacio de Estados:Es el universo de valores que pueden tomar las variables
 Precondiciones: son los asertos que deben cumplirse a la entrada de

una tarea. Si la tarea o instrucción se realiza sin que la precondición se
cumpla no tendremos garantía delos resultados obtenidos.
 Postcondiciones son los asertos acerca de los resultados que se

esperan a la salida

Verificación Vs Derivación
Verificar: demostrar que el programa construido es correcto
respecto de la especificación dada

Derivar o deducir un programa permite construir un programa a
partir de su especificación, de forma que se obtiene un algoritmo
correcto porconstrucción

Corrección Total y Corrección Parcial
Corrección parcial: {P} A {Q} es parcialmente correcto si el estado
final de A, cuando termina el programa (aunque no se exige esta
premisa), satisface {Q} siempre que el estado inicial satisface {P}.
Corrección total: Se da cuando un código además de ser correcto
parcialmente, termina.
Los algoritmos sin bucles siempre terminan por lo que lacorrección parcial implica la corrección total. Esta
distinción es esencial sólo en el caso de códigos que incluyan bucles o recursiones

Programación imperativa
Instrucciones
Asignación
Secuencia
Condicional

Iteración

Método de Verificación
Precondición más débil (pmd)

Invariante  para demostrar que un
ciclo es correcto

Instrucciones: Asignación,Secuencia, Condicional

Reglageneral:
1. Encontrar la precondición más débil {pmd} tal que

{pmd} S {Q} es válido
Pmd: conj. de todos los estados tales que desde ellos y ejecutando el programa S se llega a Q

2. Cualquier precondición {P} que implique {pmd} hace que el programa S
sea correcto
Si {P}



{pmd} entonces el programa S también es correcto para la terna
{P} S {Q}

Verificación de códigos sin buclesPara demostrar la corrección de las partes de un programa se parte de la
postcondición y a partir de ahí se deduce la precondición. El código se
verifica en sentido contrario a como se ejecuta.
{P} = PreC. Inicial
Código 1
PreC2 =PostC. 1

Código 2
PreC. 3 =PostC. 2

EJECUCION

Código 3

{ Q} =PostC. 3

VERIFICACION

Reglas para instrucciones del lenguaje
Sentencias de...