Estadísticas del PDF: TEMA 6.- VERIFICACION DE PROGRAMAS IMPERATIVOS

TEMA 6.- VERIFICACION DE PROGRAMAS IMPERATIVOS

6.1.- Lógica de Hoare.

Desarrollada por C.A.R. Hoare (1969), es una lógica que permite probar la
verdad o falsedad de propiedades de programas imperativos (especialmente
corrección y terminación) sin concurrencia o paralelismo.

Basada en la idea de diagrama de flujo anotado.

P

Q

S

• S es una “frase” de código en un programa de alto nivel, con una única

entrada y una única salida normal.

◦ Instrucción.
◦ Bloque de instrucciones consecutivas.
...