logica de hoare

2-16

´
´
CAP´
ITULO 2. ESPECIFICACION Y VERIFICACION DE PROGRAMAS.

2.2

L´gica de Hoare.
o

La l´gica de Hoare es una extensi´n de la l´gica de predicados de primer orden para
o
o
o
razonar sobre la correcci´n de programas imperativos construidos sobre una signatura
o
(S, Σ). Esta extensi´n se obtiene introduciendo un lenguaje de comandos con el que se
o
construyen losprogramas y una relaci´n especial para expresar el comportamiento de
o
un programa, as´ como un conjunto de reglas de c´lculo para la manipulaci´n de las
ı
a
o
expresiones de comportamiento.

2.2.1

Universo de programas

Sintaxis
Cada programa se construye a partir de una signatura (S, Σ) correspondiente a
los tipos de datos con los que opera, un lenguaje de comandos y una familia devariables V o variables de programa. Generalmente se supone que la signatura consta
de los universos BOOL y NAT , correspondientes a los valores l´gicos {V, F } y a los
o
n´meros naturales junto con las operaciones propias de estos universos, m´s otros pou
a
sibles universos correspondientes a tipos de datos definidos por el programador. En
todos supondremos definida una relaci´n de igualdad ‘=’que nos permite establecer
o
una equivalencia entre t´rminos del tipo correspondiente a dicho universo, con unos
e
axiomas y unas reglas de c´lculo.
a
El lenguaje de comandos que vamos a utilizar para construir programas es un lenguaje elemental que consta de unos comandos simples y unos comandos compuestos con
los cuales se construyen los t´rminos de un universo especial: el universo deprogramas
e
PRG. Los comandos simples son:
• SKIP : → PRG, o comando vac´ y
ıo,
• (· :=s ·) : Vs s → PRG, uno por cada universo s ∈ S, o comando de asignaci´n
o
de valor a variables del tipo s, donde el primer argumento es una variable de
programa del tipo s y el segundo una expresi´n del mismo tipo. En adelante suo
pondremos que las asignaciones se hacen con los tipos correctos yprescindiremos
del sub´
ındice s;
y los comandos compuestos:
• (IF · THEN · ELSE · END) : BOOL PRG PRG → PRG, o comando de selecci´n
o
simple, donde el primer argumento es un t´rmino del tipo BOOL y los otros dos
e
son programas;
• (WHILE · DO · END) : BOOL PRG → PRG, o comando de iteraci´n, donde el
o
primer argumento es un t´rmino del tipo BOOL mientras que el segundo es un
e
programa, y´
2.2. LOGICA DE HOARE.

2-17

• (· ; ·) : PRG PRG → PRG, o comando de composici´n secuencial de programas.
o
Ejemplo 2.4 Con estos comandos y una signatura correspondiente al ´lgebra de los
a
n´meros naturales con las operaciones aritm´ticas y las relaciones usuales se pueden
u
e
construir t´rminos (programas) como el siguiente:
e
X:=1;
WHILE Z>0 DO
IF (Z mod 2)=0 THEN
Y:=(Y*Y);Z:=(Z div 2)
ELSE
X:=(Y*X); Z:=Z-1
END
END

donde se han observado las normas habituales de sangrado con objeto de facilitar su
legibilidad.
Sem´ntica
a
Los t´rminos del universo de programas no se valoran de la misma forma que
e
los t´rminos correspondientes a los universos de datos, es decir, no se valoran sobre
e
un simple dominio en una interpretaci´n A de la signaturacorrespondiente, sino que
o
toman valores sobre un dominio especial: el conjunto [STAA (V ) → STAA (V )] de los
transformadores parciales de estados definidos sobre A. As´ cada programa α se valora
ı,
como un transformador de estados, escrito · [α]A ·, seg´n su estructura, de la siguiente
u
forma:
• · [SKIP]A · , transforma cada estado sta en s´ mismo, es el transformador identiı
dad;
• · [X :=t]A · , transforma cada estado sta en el estado sta(X/val A,sta (t)); es decir,
modifica el estado en la variable X asign´ndole el valor de t en el estado anterior;
a
• · [IF tB THEN α ELSE β END]A · , para cada estado sta se comporta de acuerdo
con el criterio siguiente: si A |=sta tB = V lo transforma del mismo modo que
lo hace · [α]A · y si A |=sta tB = V lo transforma del mismo modo que lo...