Departamento de Computación
Facultad de Ciencias Exactas y Naturales
Universidad de Buenos Aires
Tesis de Licenciatura en
Ciencias de la Computación
Construcciones de alto nivel como anotaciones
para la verificación automática de software
Guido de Caso - gdecaso@dc.uba.ar - L.U. 151/03
Directores: Diego Garbervetsky, Daniel Gorín
Diciembre de 2007

Resumen
La verificación automática de software es una disciplina que ha crecido mucho en los últimos años,
aportando herramientas que con bajo costo permiten aumentar la confianza que se tiene sobre un siste-
ma. En particular la verificación automática de código ha comenzado a ser una alternativa viable, pero
gran parte de las herramientas actuales se han montado sobre lenguajes preexistentes. Este enfoque ha
brindado soluciones que pueden lidiar sólo con una parte del poder expresivo de los mismos y suelen
ser introducidas mediante modificaciones ad-hoc a la sintaxis. Esta metodología no integral desfavo-
rece la adopción de estas técnicas a gran escala. Se presenta en este trabajo un lenguaje imperativo
multiprocedural muy básico cuyo diseño está orientado a la verificabilidad. Se dota a este lenguaje de
mecanismos de inferencia de precondiciones y postcondiciones que permiten asistir la tarea de anotar
ciertos fragmentos del código. Haciendo uso de estas técnicas se extiende el lenguaje con construccio-
nes de iteración de alto nivel para las cuales no es necesario proveer ningún tipo de anotación para su
verificación. Se espera que estas característiscas alivien la carga de trabajo que requiere especificar un
programa, logrando de esta forma una adopción mayor de las técnicas de verificación automática. Se
presenta un prototipo de herramienta que pone a prueba esta hipótesis, trabajando con un conjunto
diverso de demostradores de teoremas en paralelo de forma tal de maximizar la cantidad de programas
que pueden ser verificados sin intervención del programador.

A la querida memoria de Mario de Caso y Arturo Bilgray.

Agradecimientos
Esta tesis marca la finalización de una etapa que comencé hace ya casi seis años. Miro hacia atrás y
no puedo dejar de pensar en todo lo que aprendí, cuánta gente maravillosa conocí y las cosas que viví.
En primer lugar quiero agradecer a la Universidad de Buenos Aires y a todos los que, desde su
fundación hasta hoy, lucharon para que sea y siga siendo pública, gratuita, autónoma y laica.
Agradezco también a todos los grandes docentes que tuve: a Mariano Moscato, Nico Rosner, Santi
Figueira, Martín Urtasun, Vero Becher, Isabel Méndez Díaz, Javier Marenco, Sergio Mera, entre otros
tantos. Su gran entusiasmo es únicamente comparable con su capacidad de transmitir todo lo que saben.
Quiero mencionar especialmente a Charlie López Pombo y a Fer Schapachnik por confiar en mi
y brindarme la oportunidad de dar mis primeros pasos como ayudante. Fueron grandes maestros de
quienes aprendí mucho más que el arte de la docencia.
Es innumerable la cantidad de gente con la que tuve el agrado de compartir una cursada, una tarde
de estudios, una noche de programar TP, un mate en la vereda de la facu... Pablito H., Tiger, Pablo R.,
Tebi, Román, Mati, Daniel, Fran, el Pocho, Guille, el Cesaro, Monoter, Arti, Christian, Gaboto, Solcí,
Lucio, David, Germán, Manix, el Marine, Tommy, el Sabi, Eze, Lata, Toto, J, Pachi, Luigi, Pablito B.,
... A todos ellos les debo gran parte de todo lo que viví estos últimos años.
Con mis compañeros de La Mella vivimos humildes victorias y duras derrotas; nunca bajamos los
brazos. Desde hace ya más de tres años que junto con ellos laburamos, desde nuestro pequeño aporte,
todos los días para hacer más cercana una visión de universidad y de sociedad. A Piter, Ali, Leo, Charlie,
Pablo, Mateo, Laura, Nahuel y Beta: más que gracias les pido perdón por no haber podido dedicarme
todo lo que quisiera estos últimos tiempos. Con Nacho tuve también el agrado de compartir aventuras
inolvidables en nuestro viaje a lo largo de medio país.
Nuevamente quiero agradecer a Schapa por haber confiado en mi para formar parte del grupo
de desarrolladores de VInTiMe. Nunca me voy a olvidar de esos meses que pasamos con Lu y con
Andran, junto con toda la tropa de Dependex/LaFHIS: Bacardi, Lito, Dieguito P., Aspect, J, Pablo
R., Esteban, Alan, Germán, Dipi, Mati L. Agradezco particularmente a Víctor y a Seba por la confianza
que siempre me tuvieron y por la forma en la que siempre fueron abiertos a escuchar mis opiniones y
tener en cuenta mi punto de vista.
Agradezco enormemente a Juan Pablo Galeotti y a Eduardo Bonelli por lo rápida, precisa y detallada
que fue su devolución de este trabajo. Sus comentarios definitivamente sirvieron para completar, revisar,
corregir y ampliar el alcance del mismo.
Conocí a Diego Garbervetsky cuando entré en Dependex. De inmediato existía una relación de
confianza mutua, como si nos conociéramos de hace años. Vi a Diego laburar mientras dirigía a Dieguito
Piemonte, siempre muy dedicado, muy atento. Cuando su tesista estrella se recibió le pedí que me
dirija y empezamos a laburar muy de a poco pensando y repensando algunos temas. Diego siempre
confió en mi y me bancó, con todas mis inquietudes, para sacar adelante este trabajo. Hoy lo veo más

que como un director como un gran amigo.
Este trabajo nunca hubiera existido si no fuera por la idea original de Dani Gorín. Desde el principio
siempre se hizo tiempo para ayudarme con mis inquietudes a medida que iban surgiendo. Perdí la
cuenta de las veces que golpeé su puerta feliz por algún avance, triste ante un problema, frustrado,
harto, ansioso. Dani siempre estuvo ahí con alguna palabra de ánimo y alguna sugerencia. Agradezco
infinitamente todo el tiempo que le dedicó a este laburo, así como sus extensivas revisiones, ya sea desde
Buenos Aires o desde Nancy.
Realmente no encuentro palabras para darles las gracias debidamente a mis viejos. Desde que tengo
memoria ellos estuvieron ahí enseñándome lo hermoso de descubrir, conocer, aprender, pensar, leer,
jugar, repensar. Nunca faltó en mi casa algún buen disco, un libro, una peli, un juego, siempre un disfrute.
Cuando decidí emprender una carrera universitaria ellos estuvieron ahí siempre atentos, interesados aún
si cuando no entienden mucho. Para mis viejos, Cami, Mary y toda mi familia no tengo más que
agradecimiento, amor y admiración divergentes.

Índice general
1. Introducción 11
1.1. Objetivo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
1.2. Contribuciones . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
1.3. Trabajo relacionado . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
1.4. Estructura de la tesis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2. Sintaxis y semántica operacional 16
2.1. Sintaxis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
2.1.1. Expresiones . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
2.1.2. Programas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
2.1.3. Sentencias . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.2. Semántica operacional . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
2.2.1. Valuaciones . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
2.2.2. Semántica para expresiones . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
2.2.3. Semántica para sentencias . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2.2.4. Semántica para programas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2.3. Ejemplos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2.4. Conclusiones . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
3. Anotaciones como un sistema de tipos 32
3.1. Expresiones seguras . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
3.2. Semántica abstracta para sentencias . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
3.3. Programas seguros . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
3.4. Cálculo de postcondiciones y precondiciones . . . . . . . . . . . . . . . . . . . . . . . . . 40
3.4.1. Cálculo de postcondiciones . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
3.4.2. Cálculo de precondiciones . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
3.5. Reforzando anotaciones . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
3.5.1. Inferencia de especificaciones de procedimientos . . . . . . . . . . . . . . . . . . . 47
3.5.2. Fortalecimiento de invariantes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
9

Capítulo 1
Introducción
Si quieres conocer el final, mira el comienzo.
Proverbio africano
Los sistemas de software son día a día más complejos. Cada vez más aspectos de la vida cotidiana
descansan de algún modo en procesos controlados por programas. Teléfonos, juguetes, autos, aviones,
control de tráfico, entretenimiento. Su mal funcionamiento en general ocasiona disgustos y pérdidas
económicas [FPB75]. En algunos casos críticos, puede incluso ocasionar pérdidas humanas.
Asegurar el buen funcionamiento de un sistema de software es una tarea ardua. A lo largo de cuatro
decadas se utilizaron distintos enfoques con diversos grados de éxito [DHR
+
07].
El testing, por ejemplo, demostró ser útil para encontrar los errores o bugs más comunes. Sin
embargo, aplicaciones comerciales que atraviesan estrictos procesos de testing son lanzadas al mercado
con decenas de bugs.
La verificación formal garantiza la ausencia de errores de un programa respecto de su especificación.
La misma puede ser aplicada manualmente sobre pequeños ejemplos. Por ejemplo:
1: swap(x; y)
2: :? true
3: :! x = y@pre ^ y = x@pre
4: {
5: tmp x
6: x y
7: y tmp
8: }
Procedimiento swap
Se trata de un sencillo procedimiento que realiza el swap o intercambio entre dos variables enteras.
La notación :? indica la precondición y :! indica la postcondición.
Una vez definida formalmente la semántica operacional de este lenguaje podría demostrarse que,
luego de la línea 5, el valor de tmp es x@pre. De modo similar se puede ver que, luego de la línea 6, el
valor de x es y@pre. Finalmente, luego de la línea 7, el valor de y es tmp, que a su vez es x@pre.
Ciertamente este enfoque de verificación formal manual tiene serios problemas de escalabilidad, por
lo cual la automatización es una característica altamente deseable.
11

La verificación formal automatizada ha avanzado mucho en los últimos años, con casos de renombre
como por ejemplo Spec# [BLS04]. Sin embargo diversos problemas hacen que no se haya alcanzado
aún la capacidad necesaria para poder lidiar con programas a gran escala.
Por un lado, esta técnica requiere una gran cantidad de trabajo extra, en forma de anotaciones, por
parte del programador. Para cada procedimiento, método o función se debe especificar su precondición
y postcondición. Cada ciclo debe estar acompañado por su invariante y también su función variante (en
caso de querer demostrar automáticamente su terminación).
Por otra parte, el poder de demostración automática de teoremas de las herramientas actuales ha ido
en aumento, pero sigue siendo limitado. Si bien se están realizando muchos trabajos prometedores en este
área [BB04, BLM05], la capacidad actual para resolver problemas es despareja entre una herramienta y
otra; no existe una que se destaque por sobre las demás en todo contexto de uso.
1.1. Objetivo
Nuestra principal hipótesis de trabajo es que las herramientas habituales de verificación se incorporan
de manera ad-hoc a lenguajes preexistentes. Estos lenguajes fueron diseñados sin tener en cuenta la
verificabilidad de sus programas, motivo por el cual las herramientas de verificación que se construyen
sobre los mismos presentan una serie de inconvenientes.
Por un lado las anotaciones sobre comportamiento esperado aparecen como un parche al lenguaje,
siendo en varios casos presentadas a través de comentarios. Por otra parte surgen redundancias y su-
perposiciones entre los mecanismos que el lenguaje provee para asegurar su corrección: las verificaciones
sintácticas y de tipos se realizan por un lado, la verificación de especificaciones por otro.
Este aspecto asimétrico y poco prolijo que presentan estas herramientas conspiran contra la acep-
tabilidad final por parte de la industria de este tipo de técnicas. Por otra parte, si se presentaran estos
mecanismos de forma nativa e integrada, probablemente serían aceptados debido a su utilidad para evi-
tar errores. Por ejemplo los sistemas de tipos hoy en día se encuentran presentes en difundidos entornos
de desarrollo que aprovechan sus características sin generar rechazo por parte de los usuarios.
Partiendo de esta hipótesis, uno de nuestros objetivos es investigar las posibilidades que ofrece un
lenguaje de programación cuando se lo diseña en función de su verificabilidad. Para ello, es interean-
te analizar hasta dónde se puede avanzar mejorando su usabilidad sin sacrificar las capacidades de
verificación.
1.2. Contribuciones
Diseñamos un nuevo lenguaje de programación pensado como un core minimal verificable. Integra-
mos su sistema de tipos con el manejo de precondiciones y postcondiciones, eliminando de esta forma
las asimetrías que se pueden encontrar en las herramientas actuales.
Presentamos una serie de conceptos y técnicas que permiten inferir precondiciones y postcondiciones
de fragmentos de programas. Haciendo uso de estos mecanismos dotamos al lenguaje con características
que permiten asistir al usuario en la tarea de especificar ciertas partes de su código.
Adicionalmente incorporamos nuevas construcciones de iteración que no requieren anotaciones de
ningún tipo. Las mismas aprovechan los mecanismos de inferencia de precondiciones y postcondiciones
para obtener candidatos a invariantes.
Se puede entender el aporte hecho en este trabajo como dividido en dos dimensiones, o ejes. Por
12

enfoque es utilizar la relación de fuerza entre fórmulas como un elemento semántico dentro de las reglas
de tipado.
1.4. Estructura de la tesis
En el Capítulo 2 se introduce el lenguaje que es usado a lo largo de toda la tesis. Se presentan
formalmente su sintaxis y su semántica operacional. También se muestran algunos ejemplos.
Para poder realizar verificaciones de programas escritos en este lenguaje, en el Capítulo 3 se lo dota
de una noción alternativa de semántica. La misma puede ser entendida como un sistema de deducción
similar a un sistema de tipos donde un programa bien tipado es correcto con respecto a su especificación:
progresa, termina y cumple con su contrato. También se presentan mecanismos que permiten inferir
precondiciones y postcondiciones para fragmentos de programas. Aprovechando estos mecanismos se
presentan una serie de técnicas que permiten asistir la escritura de anotaciones.
Basándose en los conceptos y métodos presentados, en el Capítulo 4 se presenta la técnica que
permite ampliar el lenguaje con nuevas construcciones de iteración que no requieren especificación. Se
presentan tres casos concretos de extensiones y algunos ejemplos de su utilización donde puede verse su
capacidad de reducir la cantidad de anotaciones que deben escribirse.
En el Capítulo 5 se aplican los conceptos introducidos desde un punto de vista implementativo y se
discuten las consideraciones a tener en cuenta para llevarlos a la práctica. Asimismo, se comentan las
características principales del prototipo de herramienta que fue implementado y se muestran algunos
ejemplos de programas que pueden ser verificados utilizándolo.
Finalmente, en el Capítulo 6 se presentan las conclusiones de esta tesis y se discuten algunas alter-
nativas de trabajo a futuro.
15

2.1.1. Expresiones
Se cuenta con tres tipos distintos de expresiones:
Las expresiones enteras se utilizan para realizar asignaciones sobre variables de tipo Int, para
indexar arreglos, especificar funciones variantes, etc.
Las expresiones arreglo pueden usarse para realizar asignaciones sobre variables de tipo Array.
Las expresiones booleanas sirven como guarda para condicionales y ciclos. Se utilizan también
para especificar anotaciones tales como invariantes, precondiciones y postcondiciones.
Definición 2.3 (Expresiones enteras).
A partir de una clasificación se puede construir inductivamente IntExp, el conjunto de expresiones
enteras con variables en , tomando al más chico de todos los conjuntos que cumplen las siguientes
reglas:
(v) = Int
IE-VAR
v 2 IntExp
(v) = Int
IE-VAR@PRE
v@pre 2 IntExp
A 2 ArrayExp i 2 IntExp
IE-GET
A[i] 2 IntExp
n 2 Z
IE-NUM
n 2 IntExp
A 2 ArrayExp
IE-SIZE
jAj 2 IntExp
i1; i2 2 IntExp
IE-SUM
i1 + i2 2 IntExp
i1; i2 2 IntExp
IE-SUBS
i1 i2 2 IntExp
i1; i2 2 IntExp
IE-MUL
i1  i2 2 IntExp
i1; i2 2 IntExp
IE-DIV
i1=i2 2 IntExp
Definición 2.4 (Expresiones arreglo).
A partir de una clasificación se puede construir inductivamente ArrayExp, el conjunto de expresiones
arreglo con variables en , tomando al más chico de todos los conjuntos que cumplen las siguientes reglas:
(v) = Array
AE-VAR
v 2 ArrayExp
(v) = Array
AE-VAR@PRE
v@pre 2 ArrayExp
A 2 ArrayExp i1; i2 2 IntExp
AE-UPDATE
update A on i1 with i2 2 ArrayExp
i1; i2 2 IntExp
AE-CONST
array[i1] of i2 2 ArrayExp
Por ejemplo, si (B) = Array y (index) = Int, luego:
update B on index with 0 2 ArrayExp
(update B on index with 0)[index+ 1] 2 IntExp
17

pars(proc) para referirse a la lista de sus parámetros formales.
Pproc para referirse a la expresión booleana que representa su precondición.
Qproc para referirse a la expresión booleana que representa su postcondición.
body(proc) para referirse a la sentencia que representa su cuerpo.
2.1.3. Sentencias
En esta sección se introducen las sentencias que conforman los posibles cuerpos para un procedi-
miento. Los llamados a procedimientos son controlados de forma estática asegurándose de que existan
y la cantidad y tipo de parámetros sea adecuada. Para ello es necesario conocer qué procedimientos
ya existen, cuántos parámetros tienen, de qué tipos. El conjunto de sentencias es paramétrico en un
programa y únicamente puede llamar a procedimientos que figuren en él.
Por otra parte una sentencia puede eventualmente ampliar una clasificación para reflejar información
sobre las variables que crea. Esto se refleja en el hecho de que el conjunto de sentencias es paramétrico
en dos clasificaciones: una antes y otra después de una eventual ejecución de la sentencia.
Definición 2.7 (Sentencias).
Sea una clasificación , un programa  y otra clasificación 0.
Se puede construir inductivamente Sentence;;0 , el conjunto de sentencias que empieza con variables
en , llama potencialmente a procedimientos en  y termina con variables en 0.
Cada construcción es acompañada de una breve descripción informal, para ver su semántica operacional,
referirse a la Definición 2.17.
Se toma al más chico de todos los conjuntos que cumplen las siguientes reglas:
Asignación a una variable entera:
(v) = Int i 2 IntExp
SENT-IASSIGN
v i 2 Sentence;;
Si se sabe que el tipo de v es entero y se tiene una expresión entera, se puede asignar el valor
de tal expresión a la variable v. Observar que, la definición de expresiones admite referirse a los
valores que una variable tenía al comienzo, por ejemplo:
x (A@pre)[20] + 1
Asignación a una variable arreglo:
(v) = Array A 2 ArrayExp
SENT-AASSIGN
v A 2 Sentence;;
Similar al caso anterior, pero asignando una variable A de tipo arreglo con una expresión de tipo
arreglo.
20

Llamado a un procedimiento:
proc 2 
i 6= j ) cpi 6= cpj pars(proc) = p1; : : : ; pk
(cpi) = proc(pi)
SENT-CALL
call proc(cp1; : : : ; cpk) 2 Sentence;;
Para realizar un llamado a un procedimiento, el mismo debe estar definido en . Por otra parte,
los parámetros concretos cpi deben ser provistos sin repetidos, en cantidad y tipos adecuados con
respecto a los parámetros formales pi.
Observar que si se permitieran repetidos entre los parámetros formales se estaría produciendo
aliasing, lo cual dificulta la verificación de programas ampliamente.
Utilizaremos además las siguientes abreviaturas:
Asignación de un elemento en un arreglo:
v[i1] i2
def
= v (update v on i1 with i2)
Siempre y cuando (v) = Array.
Condicionales sin rama else:
if g then s fi
def
= if g then s else skip fi
Observación 2.1. La forma en la que se construyen los programas, a partir de extensiones con nuevos
procedimientos cuyo cuerpo llama a procedimientos que ya existen, asegura la ausencia de recursión.
A lo largo del resto de la tesis se usa el concepto de variables locales de una sentencia, definido a
continuación.
Definición 2.8 (Variables locales).
Se llama localVars a la función que, dada una sentencia s 2 Sentence;;0 , devuelve el conjunto de
variables locales a la misma. O sea, el conjunto de variables creadas por s, definido como:
localVars(s) = dom(0)r dom()
2.2. Semántica operacional
Se introduce en esta sección el concepto de ejecución de una sentencia. Con tal fin, es necesario
primero introducir el concepto de valuación, que sirve para conocer el valor de cada una de las variables
de un programa. Se puede pensar una valuación como la abstracción de la memoria en una computadora
convencional.
22

array : fA j (A) = Arrayg ! A
Determina el valor actual de cada variable arreglo en .
array@pre : fA j (A) = Arrayg ! A
Determina el valor al comienzo de cada variable entera en .
Las asignaciones y otras operaciones alteran el valor actual para algunas variables. Es necesario que
las valuaciones puedan ser extendidas para reflejar estos efectos sobre las variables.
Definición 2.11 (Extensiones a una valuación).
Se definen las siguientes extensiones a una valuación  2 M:
Si (v) = Int y n 2 Z, luego:
0 = fv 7! ng
es una valuación en M donde el único cambio es que int
0(v) = n.
Si v =2 dom() y n 2 Z, luego:
0 = fint v 7! ng
es una valuación en Mfv 7!Intg donde los cambios son que:
int
0(v) = int@pre
0(v) = n
Si (v) = Array y A 2 A, luego:
0 = fv 7! Ag
es una valuación en M donde el único cambio es que array
0(v) = A.
Si v =2 dom() y A 2 A, luego:
0 = farray v 7! Ag
es una valuación en Mfv 7!Arrayg donde los únicos cambios son que:
array
0(v) = array@pre
0(v) = A
Otras veces es necesario que una valuación olvide los valores que asigna a algunas variables.
Definición 2.12 (Olvido en una clasificación).
Dada una clasificación y un conjunto de variables V  dom() se define el olvido en una clasificación,
notado V que resulta de olvidar la clasificación para las variables en V .
V (v) =
(
(v) si v =2 V
indefinido sino
Definición 2.13 (Olvido en una valuación).
Dada una valuación  2 M y un conjunto de variables V  dom() se define el olvido en una valuación,
notado  V 2 M V que resulta de olvidar los valores para las variables en V .
 V (v) =
(
(v) si v =2 V
indefinido sino
24

Definición 2.16 (Semántica para expresiones booleanas).
Dadas una valuación  2 M y una expresión booleana b 2 BoolExp, se usa JbK
Bool
 = x para denotar
que la semántica de b bajo la valuación  está bien definida y su valor es x 2 ftrue; falseg.
Ji1KInt = n Ji2K
Int
 = n
S-BE-IEQ-T
Ji1 = i2KBool = true
Ji1KInt = n Ji2K
Int
 = m n 6= m
S-BE-IEQ-F
Ji1 = i2KBool = false
JA1KArray = A JA2K
Array
 = A
S-BE-AEQ-T
JA1 = A2KBool = true
JA1KArray = A JA2K
Array
 = B A 6= B
S-BE-AEQ-F
JA1 = A2KBool = false
Ji1KInt = n Ji2K
Int
 = m n < m
S-BE-ILT-T
Ji1 < i2KBool = true
Ji1KInt = n Ji2K
Int
 = m n  m
S-BE-ILT-F
Ji1 < i2KBool = false
Jb1KBool = true Jb2K
Bool
 = true
S-BE-AND-T
Jb1 ^ b2KBool = true
Jb1KBool = true Jb2K
Bool
 = false
S-BE-AND-F1
Jb1 ^ b2KBool = false
Jb1KBool = false
S-BE-AND-F2
Jb1 ^ b2KBool = false
JbKBool = false
S-BE-NOT-T
J:bKBool = true
JbKBool = true
S-BE-NOT-F
J:bKBool = false
todo n 2 Z cumple que JbKBoolfint v 7!ng = true
S-BE-IFORALL-T
J8 v : Int (b)KBool = true
algún n 2 Z cumple que JbKBoolfint v 7!ng = false
S-BE-IFORALL-F
J8 v : Int (b)KBool = false
todo A 2 A cumple que JbKBoolfarray v 7!Ag = true
S-BE-AFORALL-T
J8 v : Array (b)KBool = true
algún A 2 A cumple que JbKBoolfarray v 7!Ag = false
S-BE-AFORALL-F
J8 v : Array (b)KBool = false
Observación 2.2. Observar que dada una valuación  y una expresión entera i, JiKInt es computable.
Del mismo modo, siendo A una expresión arreglo, JAKArray también lo es.
Sin embargo, si se toma b una expresión booleana, JbKBool no es computable debido a la combinación
de cuantificación con expresiones aritméticas. Si b es libre de cuantificadores, su semántica es computable.
26

Para realizar un llamado, es necesario primero construir una valuación auxiliar  con el binding
de los parámetros concretos cp1; : : : ; cpk con los formales pars(proc) = p1; : : : ; pk. La misma se
obtiene usando:
(pi)
def
= (cpi)
(pi@pre)
def
= (cpi)
Suponer que la valuación auxiliar  logra satisfacer la precondición del procedimiento llamado,
y el cuerpo del mismo ejecuta correctamente y termina en una valuación 0 tal que satisface la
postcondición.
Los parámetros concretos son reasignados según el valor en 0, por lo tanto 0 es igual a  a
excepción de los valores para los parámetros concretos, los cuales se obtienen de 0 de la siguiente
manera:
0(cpi)
def
= 0(pi)
2.2.4. Semántica para programas
Se introduce el concepto de ejecución de un programa. Puede verse como un llamado a un procedi-
miento inicial cualquiera.
Definición 2.18 (Semántica para programas).
Se usa  .  : proc . 0 para denotar la semántica de un programa  iniciando en un procedimiento proc,
partiendo de la valuación  2 Mproc , finalizando su ejecución y obteniendo la valuación 
0 2 Mproc .
Su definición es dada por la siguiente regla:
proc 2  JPprocKBool = true  . body(proc) . 
0 JQprocK
Bool
0 = true
SEM-PROG
 .  : proc . 0 localVars(body(proc))
Observar que se toma como valuación final 0, sin embargo se olvida el valor de las variables locales al
cuerpo del procedimiento.
2.3. Ejemplos
Se muestran a continuación algunos ejemplos de pequeños programas escritos en el lenguaje de
programación presentado.
El primer ejemplo calcula el cociente y resto de dos naturales a y b.
29

Por ejemplo:
safeI(A[x] + jupdate A on 8 with 15j)  0  x < jAj ^ 0  8 < jAj
Se utiliza el símbolo  ya que en realidad se ha simplificado la expresión eliminando los true de las
conjunciones.
Teorema 3.1 (Las condiciones para expresiones seguras son correctas).
Sean i 2 IntExp; A 2 ArrayExp; b 2 BoolExp. Sea  2 M, luego:
si JsafeI(i)KBool = true luego existe algún n 2 Z : JiK
Int
 = n
si JsafeA(A)KBool = true luego existe algún A 2 A : JAK
Array
 = A
si JsafeB(b)KBool = true luego existe algún x 2 ftrue; falseg : JbK
Bool
 = x
Dem:
Se demuestra por inducción estructural. Los detalles concretos pueden verse en la Sección A.1.
2
3.2. Semántica abstracta para sentencias
Antes de definir la semántica basada en transformación de estados genéricos es necesario introducir
dos nociones que serán usadas en el resto de este trabajo.
La primera de ellas es la noción de fuerza entre expresiones booleanas.
Definición 3.4 (Relacion de fuerza entre expresiones booleanas).
Dadas dos expresiones booleanas b1; b2 2 BoolExp, se dice que b1 fuerza a b2 si toda valuación  2 M
tal que Jb1KBool = true también cumple que Jb2K
Bool
 = true.
Se nota b1 j= b2.
Por ejemplo:
x  10 ^ z < 15 j= x  8
Observación 3.1. Observar que dadas dos expresiones booleanas b1; b2 2 BoolExp, determinar si
b1 j= b2 es, en general, no decidible. Esto se debe a que una expresión booleana puede codificar la
aritmética de Peano, para la cual no hay un método de decisión.
La segunda de estas nociones es la sustitución en expresiones.
Definición 3.5 (Sustitución en expresiones).
Sea i 2 IntExp y sean e; e
0
dos expresiones del mismo tipo. Se define la sustitución en i de todas las
apariciones de e por e0, notada ibe 7! e0c.
ibe 7! e0c
def
= e0 si i = e
34

Se define a continuación la semántica abstracta para una sentencia. Esta noción trabaja con valua-
ciones simbólicas representadas mediante expresiones booleanas.
La semántica operacional definida en el capítulo anterior permite establecer la transformación que
realiza una sentencia sobre una valuación concreta, o sea una ejecución. En el caso de la semántica
abstracta se presenta una transformación entre la expresión booleana que caracteriza una valuación
simbólica antes y después de la ejecución de una sentencia; se trata de caracterizar un conjunto poten-
cialmente infinito de ejecuciones.
Definición 3.6 (Semántica abstracta para sentencias).
Dadas p 2 BoolExp, s 2 Sentence;;0 y q 2 BoolExp0 se usa fpg s fqg para notar la semántica
abstracta de una sentencia s partiendo de una expresión booleana p y llegando a otra q.
Asignación a una variable entera:
p j= safeI(i) 9 v0 : Int (pbv 7! v0c ^ v = ibv 7! v0c) j= q
A-SENT-IASSIGN
fpg v i fqg
Se le puede dar semántica abstracta a una asignación desde p a q si sucede que:
 p es suficiente para garantizar que la expresión entera i está bien definida.
 Se utiliza v0 para representar el valor que tenía la variable v previo a la asignación. Se
reemplazan las apariciones de v por v0 en la expresión p de forma tal de preservar todo lo
que se conocía. Por otra parte, luego de la asignación se cumple que v tiene el valor de la
expresión i, tomando el recaudo de reemplazar allí también la variable v por su valor anterior
v0.
Observar que esta regla admite como consecuencia una expresión q siempre y cuando esta sea
igual o más débil que el efecto de la asignación sobre la expresión p.
Asignación a una variable arreglo:
p j= safeA(A) 9 v0 : Array (pbv 7! v0c ^ v = Abv 7! v0c) j= q
A-SENT-AASSIGN
fpg v A fqg
Similar al caso anterior, pero para arreglos.
Creación de una variable entera:
p j= safeI(i) p ^ v = i j= q
A-SENT-IDEF
fpg int v i fqg
El caso de la creación de una nueva variable es similar a la asignación. La única diferencia es que
ya no es necesario introducir un existencial para recordar el viejo valor de la variable v, ya que
ésta no existe previo a la definición.
36

 El invariante vale al comienzo, o sea que p fuerza el invariante.
 El invariante y el hecho de que la guarda vale satisfacen una cierta expresión p0 que representa
el estado al comenzar una iteración genérica. Dicha expresión p0 es tal que garantiza que el
variante es positivo.
 Al cuerpo del ciclo se le incorpora una asignación para recordar el valor del variante inicial.
Tal cuerpo aumentado tiene semántica abstracta entre p0 y otra expresión booleana q0. Esto
representa la transformación de estados de una ejecución genérica.
 Dicha expresión q0 preserva el invariante y hace que el variante decrezca.
 Por último, el invariante y la negación de la guarda fuerzan q.
Llamado a un procedimiento:
1  i  k pbcpi 7! pic j= Pproc
9o1; : : : ; ok (pbcpi 7! oic ^ Qprocbpi 7! cpi; pi@pre 7! oic) j= q
A-SENT-CALL
fpg call proc(cp1; : : : ; cpk) fqg
Observar que puede asumirse sin perder generalidad que los parámetros formales pars(proc) =
p1; : : : ; pk son disjuntos con respecto a todas las otras variables que puedan aparecer en el progra-
ma.
Un llamado a procedimiento tiene semántica abstracta entre p y q si:
 Reemplazando en p los parámetros concretos cpi por los formales pi se puede garantizar la
precondición del procedimiento proc.
 Tal como en el caso de una asignación, sigue valiendo p, pero sobre ciertos valores viejos para
los parámetros concretos, denominados oi en la regla. Por otra parte vale la postcondición
del procedimiento, donde se sustituyen los parámetros formales por los concretos, y el valor
inicial de los parámetros formales por oi, o sea los valores viejos de los parámetros concretos.
En esta regla se comete un abuso de notación al realizar k sustituciones simultáneas. Esto no es
problema ya que se trata de todas expresiones distintas.
Observar que todos los consecuentes de las reglas para la semántica abstracta son de la forma
fpg s fqg sin instanciar p ni q. De esta forma las reglas pueden entenderse de forma reversible como
una transformación hacia adelante o hacia atrás, según como se las mire. Aprovecharemos esta
característica en la Sección 3.4.
Los siguientes casos sirven a modo de ejemplo para apreciar el funcionamiento de estas reglas:
fx = 10g x x+ 1 f9 x0 : Int (x0 = 10 ^ x = x0 + 1)g
En este primer caso se aplica la regla de la asignación de enteros, dejando como consecuencia (q en la
regla) la expresión más fuerte posible. Sería lógicamente equivalente decir que la consecuencia es x = 11.
ftrueg if true then a 1 else a 0 fi fa = 1g
El condicional siempre tomará la rama then, por ende se obtiene el resultado de la misma como
consecuencia.
38

Teorema 3.2 (Los programas seguros tienen semántica operacional bien definida).
Sea un programa seguro  y sea p un procedimiento en . Luego:
para toda valuación  2 Mp sucede que si JPpK
Bool
 = true
luego existe una valuación 0 2 Mp tal que  .  : p . 
0
y JQpK
Bool
0 = true
Dem:
Se demuestra por inducción estructural, los detalles se pueden encontrar en la Sección A.3.
2
Recordar que la definición de semántica operacional que presentamos en el capítulo anterior determi-
na que una ejecución es correcta sólo si no se viola ninguna anotación y nunca una expresión se indefine.
Por ende, un programa seguro siempre será correcto respecto de su especificación.
3.4. Cálculo de postcondiciones y precondiciones
La semántica abstracta puede entenderse como una ejecución a través de transformaciones de ex-
presiones booleanas que predican sobre el valor de las variables. Este concepto es utilizado para definir
programas seguros, que son aquellos para los cuales sus ejecuciones siempre están bien definidas.
Otra forma de entender la semántica abstracta es como un mecanismo de prueba similar a un sistema
de tipos. Así, podríamos decir que si se llega al juicio fpreg s fpostg para cada uno de los procedimientos,
luego se trata de un programa seguro o tipable y por ende se ejecutará correctamente.
Al tener un sistema de tipos siempre es deseable automatizar la inferencia de juicios utilizando sus
reglas. En esta sección introducimos dos cálculos: dada una sentencia s uno obtendrá una postcondición
de la misma a partir de una expresión de comienzo; el otro obtendrá una precondición a partir de una
expresión de llegada. Estos cálculos pueden ser vistos como mecanismos de inferencia para el sistema
de tipos representado por la semántica abstracta.
Sin embargo aún contando con estos cálculos, estos dependerían de la relación de fuerza j=, la
cual es no decidible. En el Capítulo 1 mencionamos que existen herramientas que permiten resolver
automáticamente este problema de manera parcial en una cantidad de casos interesantes. O sea, dadas
dos expresiones booleanas b1 y b2, hay 3 resultados posibles:
Valid significa que se pudo probar que b1 j= b2.
Not valid significa que se pudo probar que no es cierto que b1 j= b2.
Unknown significa que no se sabe si b1 j= b2 o no.
Observar que, permitiendo la tercera respuesta, este es un problema decidible
1
, y existen herramien-
tas que permiten resolver sin devolver Unknown cada vez más instancias de este problema. Por ahora
se asumirá que estas herramientas constituyen un oráculo y que en caso de que retorne Unknown no se
podrá continuar con la verificación. En el Capítulo 5 se comentará en mayor detalle cómo se utilizaron
estas herramientas, intentando minimizar las respuestas de tipo Unknown.
Asumiendo por ahora que el oráculo se comporta de forma adecuada, cerramos formalmente el círculo
del proceso de verificación. Los cálculos de postcondiciones y precondiciones permiten capturar juicios
1
En particular se puede realizar una implementación que siempre devuelva Unknown.
40

acerca de la semántica abstracta; la semántica abstracta permite establecer si un programa es seguro;
un programa seguro sólo tiene ejecuciones que terminan; las ejecuciones terminan sólamente si no violan
ninguna anotación.
Antes de definir los cálculos para precondiciones y postcondiciones es necesario introducir la clausura
existencial de una fórmula con respecto a un conjunto de variables.
Definición 3.8 (Clausura existencial).
Dada una expresión booleana b 2 BoolExp y un conjunto de variables V  dom(), se define la
clausura existencial Cl9V (b) 2 BoolExp V de la siguiente forma:
Cl9V (b) = 9 i1; : : : ; in : Int (9 A1; : : : ; Am : Array (b))
Donde fi1; : : : ; ing son las variables enteras en V y fA1; : : : ; Amg son las variables arreglo en V .
3.4.1. Cálculo de postcondiciones
Definimos a continuación la postcondición calculada. La misma se obtiene utilizando una versión
especializada de las reglas de semántica abstracta, para las cuales la expresión booleana de partida o
precondición está fijada.
Primero se introducen las reglas, luego se comentan algunos ejemplos y finalmente presentamos un
resultado que vincula este cálculo con la semántica abstracta.
Definición 3.9 (Postcondición calculada).
Sea  un programa seguro, s 2 Sentence;;0 y p 2 BoolExp se define la postcondición de la sentencia
s con respecto a la expresión booleana p, notada post(s; p) 2 BoolExp0 .
Asignaciones:
p j= safeI(i)
POST-IASSIGN
post(v i; p) = 9 v0 : Int (pbv 7! v0c ^ v = ibv 7! v0c)
p j= safeA(A)
POST-AASSIGN
post(v A; p) = 9 v0 : Array (pbv 7! v0c ^ v = Abv 7! v0c)
En estos casos las reglas son muy similares a las de la semántica abstracta; entre todas las expre-
siones booleanas de llegada q que permitían, se utiliza la más fuerte posible.
Creación de variables:
p j= safeI(i)
POST-IDEF
post(int v i; p) = p ^ v = i
p j= safeA(A)
POST-ADEF
post(array v A; p) = p ^ v = A
Tal como en el caso de las asignaciones, se utiliza el q más fuerte posible.
41

En cambio, si se parte de una expresión booleana más precisa:
post(if x = 0 then x 1 else x 0 fi; x > 0) =
= 9 x0 : Int (x0 > 0 ^ x0 = 0 ^ x = 1) _ 9 x0 : Int (x0 > 0 ^ x0 6= 0 ^ x = 0) j=
j= x = 0
Otro ejemplo interesante es ver qué sucede en el caso de toparse con un ciclo. Por ejemplo:
post(while i > 0
| {z }
g
:?! i  0
| {z }
inv
:# i|{z}
var
do i i 1
| {z }
s
od; i = 10
| {z }
p
)
Para resolver este caso es necesario asegurarse primero de satisfacer todas las hipótesis de la regla
POST-WHILE.
true j= safeB(inv) ; true j= true
inv j= safeB(g) ; i  0 j= true
inv j= safeI(var) ; i  0 j= true
p j= inv ; i = 10 j= i  0
inv ^ g j= var > 0 ; i  0 ^ i > 0 j= i > 0
post(var0 i i i 1; i  0 ^ i > 0)  9 i
0 : Int (i0 > 0 ^ var0 = i
0 ^ i = i0 1)
| {z }
q0
q0 j= inv ; 9 i0 : Int (: : :) j= i  0
q0 j= var < var0 ; 9 i
0 : Int (: : :) j= i < var0
Puede comprobarse que efectivamente todas estas relaciones de fuerza se satisfacen. De esta manera
la postcondición calculada sería:
post(while i > 0 :?! i  0 :# i do i i 1 od; i = 10) = i  0 ^ i  0  i = 0
Estas reglas que definen el cálculo de postcondiciones son compatibles con la noción de semántica
abstracta. En otras palabras, la inferencia que realizan es correcta con respecto al sistema de tipos
introducido. Presentamos este resultado a continuación.
Teorema 3.3 (El cálculo de postcondiciones respeta la semántica abstracta).
Sea s 2 Sentence;;0 y sea p 2 BoolExp. Si post(s; p) = q luego fpg s fqg.
Dem:
Un esbozo de su demostración por inducción estructural puede hallarse en la Sección A.4.
2
Tal como se mencionó al abrir esta sección, con este mecanismo se puede capturar el concepto de
programa seguro como aquel para cual todos sus procedimientos proc(p1; : : : ; pk) :? pre :! post f s g
cumplen que:
post(s; pre) j= post
43

 La guarda es verdadera y se satisface la precondición de la rama then para llegar a q.
 La guarda es falsa y se satisface la precondición de la rama else para llegar a q.
Ciclo:
true j= safeB(inv) inv j= safeB(g) inv j= safeI(var)
inv ^ g j= p0 p0 j= var > 0
post(var0 var s; inv ^ g) = q
0
q0 j= inv q0 j= var < var0 inv ^ :g j= q
PRE-WHILE
pre(while g :?! inv :# var do s od; q) = inv
Para obtener la precondición de un ciclo se pide, de forma muy similar al caso de la postcondición
de un ciclo, que se cumpla el teorema del invariante
2
.
Por otra parte se pide que la salida del ciclo, dada por inv ^ :g sea suficiente para probar la
postcondición deseada q. En ese caso la precondición del ciclo será su invariante.
Esta regla no garantiza que la precondición sea la más débil posible. Sólo se trata de una forma
de proseguir hacia arriba obteniendo una posible precondición que permita llegar a q.
Llamado a un procedimiento:
1  i  k
PRE-CALL
pre(call proc(cp1; : : : ; cpk); q) = Pprocbpi 7! cpic ^
(9a1; : : : ; ak(Qprocbpi 7! ai; pi@pre 7! cpic ^ qbcpi 7! aic))
Es necesario que se cumpla la precondición del procedimiento llamado con las sustituciones de los
parámetros formales por los concretos.
Por otra parte es necesario que la postcondición del procedimiento pueda forzar q, realizando las
sustituciones de parámetros formales por los concretos. Tener en cuenta el reemplazo de parámetros
anteriores por sus valores cuantificados, tal como en la regla para la semántica abstracta.
Por ejemplo:
pre(j j + 1; i = j ^ j = 20) =
= true ^ i = j + 1 ^ j + 1 = 20 j=
j= i = 20 ^ j = 19
Otro ejemplo interesante es el caso de un ciclo. Observar el mismo ejemplo que se usó para el cálculo
de postcondiciones:
pre(while i > 0 :?! i  0 :# i do i i 1 od; i = 0) = i  0
2
Observar que para verificar esta condición se utiliza el cálculo de postcondiciones. Podría haberse utilizado el cálculo
de precondiciones, pero en ese caso la regla sería más difícil de seguir y muy distinta con respecto a la regla de semántica
abstracta para este caso. Esta diferencia hubiera dificultado la prueba del resultado que vincula este cálculo con la
semántica abstracta.
45

3.5. Reforzando anotaciones
Hasta aquí en este capítulo presentamos formalismos que capturan el comportamiento de las eje-
cuciones mediante transformaciones de estados, representados con expresiones booleanas. Los cálculos
de postcondiciones y precondiciones permiten obtener formas efectivas de recorrer una sentencia hacia
adelante o hacia atrás respectivamente. Con algoritmos adecuados y usando el oráculo tal como se
verá en el Capítulo 5 se puede llegar a determinar si un programa es seguro.
Ya se mencionó que para realizar este tipo de verificaciones de corrección y terminación es indispen-
sable que las anotaciones introducidas por el programador sean suficientemente precisas. Esto genera
una carga de trabajo extra que en muchos casos podría llegar a ser considerada como una molestia.
Haciendo uso de los cálculos que presentamos en la sección anterior, a continuación introducimos dos
técnicas que permiten aliviar esta carga de trabajo. La primera de ellas es la inferencia de precondiciones
y postcondiciones de procedimientos. La segunda es el fortalecimiento de invariantes de ciclos.
3.5.1. Inferencia de especificaciones de procedimientos
La primera de las técnicas que tienen como objetivo aliviar la carga de especificación es la inferencia
de precondiciones y postcondiciones.
Observar el siguiente procedimiento:
1: inc(x)
2: :? true
3: :! x = x@pre+ 1
4: {
5: x x+ 1
6: }
Incrementar en uno
Dado que contamos con una forma de inferir postcondiciones de una sentencia el programador podría
ahorrarse la tarea de escribir la postcondición del procedimiento. En particular podría inferirse:
post(x x+ 1; x = x@pre) = 9 x0 : Int (x0 = x@pre ^ x = x0 + 1)
Y esta postcondición inferida es equivalente a la postcondición del procedimiento del ejemplo, si bien es
más larga y engorrosa de leer. Observar que en cambio de partir desde true se partió desde x = x@pre,
lo cual siempre es válido para todos los parámetros al comenzar la ejecución.
Observar este otro procedimiento:
1: div(a; b; r)
2: :? b 6= 0
3: :! r = a=b ^ a = a@pre ^ b = b@pre
4: {
5: r a=b
6: }
División entera
Suponer por un momento que no se cuenta con especificación alguna para este procedimiento y se
quiere inferir la misma a partir de la sentencia r a=b. Se puede comenzar por obtener una precondición
47

que garantice que se alcance a completar la ejecución, o sea la precondición calculada con respecto a
alcanzar true.
pre(r a=b; true) = safeI(a=b) = b 6= 0
Una vez obtenida esta precondición, se puede partir desde allí para obtener la postcondición del
procedimiento.
post(r a=b; b 6= 0 ^ a = a@pre ^ b = b@pre ^ r = r@pre) =
9 r0 : Int (b 6= 0 ^ a = a@pre ^ b = b@pre ^ r0 = r@pre ^ r = a=b)
Nuevamente la postcondición obtenida por este método es equivalente a la que el programador hubiera
escrito en primer término.
En general podremos inferir la especificación de un procedimiento aunque la calidad resultante
dependerá de la precisión de los invariantes de los ciclos.
Por ejemplo tomar el caso de un programa que incrementa en uno todos los elementos de un arreglo.
Si el invariante de ese ciclo únicamente dice que la variable de iteración utilizada está en rango, luego
la postcondición no podrá capturar el hecho de que los elementos del arreglo fueron incrementados.
La definición siguiente permite inferir especificaciones en el caso en que tanto la precondición como
la postcondición sean desconocidas. Realizarlo cuando alguna de estas dos anotaciones se encuentra
presente son casos más sencillos que no serán desarrollados.
Definición 3.11 (Inferencia de especificación).
Sea proc(p1; : : : ; pk) :? _ :! _ f s g un procedimiento con precondición y postcondición desconocidas.
Sean:
P = pre(s; true)
Q = post(s; P ^ p1 = p1@pre ^ : : : ^ pk = pk@pre)
Se dice que P es la precondición inferida de proc y Q es su postcondición inferida.
La inferencia de especificaciones presentada realiza una única pasada hacia arriba y luego hacia
abajo. Podría realizarse algún tipo de cálculo de punto fijo realizando pasadas sucesivas hasta que la
precondición y la postcondición inferida no sufran cambios. Esta alternativa no ha sido desarrollada,
sin embargo intuimos que sería necesario algún mecanismo que asegure la convergencia, probablemente
mediante la utilización de aproximaciones (conocidas como widenings) utilizando la relación de fuerza
j=.
3.5.2. Fortalecimiento de invariantes
En esta sección introducimos una traducción que aumentará la precisión de los invariantes que
acompañan los ciclos. La idea intuitiva es incorporar en los invariantes información relativa al punto de
entrada a los mismos.
Por ejemplo, si se sabe que antes de llegar a un ciclo una variable j siempre vale 10 y se sabe que el
ciclo no toca tal variable, puede agregarse j = 10 al invariante.
Antes de presentar esta técnica es primero necesario tener una forma de obtener las variables que
una sentencia modifica. En el caso general esto es no decidible ya que por ejemplo habría que poder
48

resolver qué rama toma un condicional. Sin embargo se puede sobreaproximar de manera sintáctica el
conjunto de variables modificadas, obteniendo el conjunto de variables potencialmente modificadas por
una sentencia.
Definición 3.12 (Variables potencialmente modificadas).
Se llama modVars a la función que, dada una sentencia s 2 Sentence;;0 , devuelve el conjunto de
variables potencialmente modificadas por la misma, definido como:
modVars(v i) = fvg
modVars(int v i) = fvg
modVars(v A) = fvg
modVars(array v A) = fvg
modVars(skip) = ;
modVars(s1 s2) = modVars(s1) [modVars(s2)
modVars(if g then s1 else s2 fi) = modVars(s1) [modVars(s2)
modVars(while g :?! inv :# var do s od) = modVars(s)
modVars(call proc(cp1; : : : ; cpk)) = fcpi j pi 2 modVars(body(proc))g
Por ejemplo:
modVars(if true then a 4 else b 0 fi) = fa; bg
Definición 3.13 (Traducción de sentencias).
Dada una sentencia s 2 Sentence;;0 la misma puede ser traducida para obtener otra cuyos invariantes
sean más precisos. Se llamará trS(s; p) a la traducción de la sentencia s asumiendo que antes de su
ejecución siempre es válida la expresión booleana p 2 BoolExp.
La traducción no afecta ninguna de las sentencias básicas tales como asignaciones, sentencia vacía o
llamado a procedimientos.
trS(v i; p)
def
= v i
trS(v A; p)
def
= v A
trS(int v i; p)
def
= int v i
trS(array v A; p)
def
= array v A
trS(skip; p)
def
= skip
trS(call proc(cp1; : : : ; cpk); p)
def
= call proc(cp1; : : : ; cpk)
Al secuenciar sentencias se traduce la primera en base a p. Luego se traduce la segunda en base a la
postcondición de la traducción de la primera.
trS(s1 s2; p)
def
= S1 tr
S

s2; post(S1; p)

donde S1 = tr
S(s1; p)
Ante un condicional se traducen ambas ramas a partir de p y el valor correspondiente de la guarda.
trS(if g then s1 else s2 fi; p)
def
= if g then trS(s1; p ^ g) else tr
S(s2; p ^ :g) fi
49

Una de las técnicas presentadas permite aumentar la precisión de los invariantes, sin embargo lo
hace aumentándolos con información sobre las variables que no modifica el ciclo. Sigue siendo necesario
aportar a mano un invariante que predique sobre las variables que el ciclo modifica.
Hay una serie de tareas relativamente frecuentes para las cuales se suelen utilizar ciclos que obedecen
a ciertos patrones. Inicializar todos los elementos de un arreglo o sumarle 3 a cada uno de ellos son dos
tareas muy similares. El invariante en estos dos casos sería casi idéntico. Copiar un arreglo tampoco
diferiría mucho.
En el capítulo siguiente presentaremos nuevas construcciones para el lenguaje. Las mismas permiten
escribir de forma concisa este tipo de tareas para las cuales el invariante es inferible utilizando templates.
En caso de que el programador opte por usar estas construcciones, puede obviar la tarea de proveer
invariante y variante. De esta forma se reduce al mínimo la necesidad de anotar el código con el objetivo
de verificarlo automáticamente.
51

Capítulo 4
Construcciones de alto nivel como
anotaciones
Language is not an abstract construction of the learned, or of dictionary makers, but is something arising out
of the work, needs, ties, joys, affections, tastes, of long generations of humanity, and has its bases broad and
low, close to the ground.
Noah Webster
En los dos capítulos anteriores presentamos un lenguaje que cuenta con anotaciones que permiten
realizar verificaciones de corrección y terminación. Para que estas verificaciones puedan llevarse a cabo
con éxito, las anotaciones provistas deben ser suficientemente precisas y esto supone una carga de trabajo
extra.
En el Capítulo 3 introdujimos mecanismos que permiten calcular una precondición (o una postcon-
dición) a partir de una sentencia dada. El objetivo de este capítulo es combinar estos mecanismos de
forma tal de obtener nuevas construcciones de iteración que no requieran que se provea un invariante ni
una función variante.
El lenguaje presentado, como sucede con casi todos los lenguajes imperativos, se encuentra muy
ligado a la arquitectura de las computadoras. Las estructuras de control condicionales y de iteración
son un reflejo refinado de las instrucciones básicas que tienen los microprocesadores.
En otros paradigmas, tales como la programación funcional y crecientemente la programación orien-
tada a objetos, las estructuras de recursión y control respectivamente, han evolucionado.
En Haskell [HPF99], por ejemplo, se trabaja con patrones de recursión tales como map, que
permite aplicar una función a cada elemento en una lista; o filter, que preserva de una lista únicamente
aquellos elementos que cumplen un cierto criterio.
En Smalltalk [GR83] existen diversos patrones de iteración tales como select, collect, inject. Los
mismos son implementados como mensajes a ciertos objetos, que permiten realizar tareas tales como
filtrar una colección según un criterio, aplicar una función a cada elemento, etc.
Incluso Java, un lenguaje masivamente usado, ha sido extendido en su versión 5.0 [Aus04] con
una construcción de tipo for each que evita la utilización de un índice o iterador al recorrer cualquier
colección.
Todos estos son ejemplos de tareas que podrían ser realizadas con un ciclo tradicional (o recursión
explícita en el caso de Haskell). Sin embargo las versiones más específicas son preferibles ya que:
52

Incrementar un arreglo en 1
1: firstN(A)
2: :? jAj > 0
3: :! 8k = 0  k < jAj : A[k] = k
4: {
5: int i 0
6: while i < jAj
7: :?! 0  i  jAj ^
8: 8k = 0  k < i : A[k] = k ^
9: 8k = i  k < jAj : A[k] = A@pre[k]
10: :# jAj i
11: do
12: A[i] i
13: i i+ 1
14: od
15: }
Lista de los primeros naturales
El primero de ellos incrementa en 1 todos los elementos de un arreglo. El segundo retorna la lista de
los primeros n naturales, donde n está dado por el tamaño del arreglo que se recibe como parámetro.
En principio estos dos programas calculan un resultado muy diferente. Sin embargo, la forma en que
llegan a tal resultado es en gran medida similar. Se recorre todo el arreglo, realizando una tarea sobre
cada uno de los elementos del mismo.
Los programas coinciden en que:
El cuerpo del ciclo realiza una transformación sobre un elemento del arreglo. La misma no depende
de otros elementos del arreglo.
Se cuenta con una variable de iteración i que cumple que:
1. Comienza en 0.
2. Se itera mientras valga menos que jAj.
3. Se incrementa al final de cada iteración.
4. No es alterada por la transformación que se hace a cada elemento del arreglo A.
El invariante especifica que:
1. La variable de iteración i está en rango.
2. Todos los elementos ya visitados han sufrido la transformación.
3. Todos los elementos aún no visitados permanecen intactos.
El variante indica que se está recorriendo el arreglo hacia adelante.
La postcondición indica que todos los elementos del arreglo sufrieron la transformación.
Este tipo de iteración puede ser codificada con una metasentencia map, la cual se presenta a conti-
nuación.
54

Definición 4.1 (Metasentencia map).
Sea una clasificación tal que (A) = Array e i =2 dom().
Sea s 2 Sentencefi 7!Intg;;0 una sentencia tal que su conjunto de variables potencialmente modifica-
das modVars(s) contiene únicamente variables locales y a A. Más específicamente, se debe garantizar
sintácticamente que A es modificado únicamente en la posición i. Adicionalmente, s sólo puede acceder
a A para obtener dicha posición o para obtener su tamaño.
Luego, se define la metasentencia map:
map s in A[.. i ..]
Se trata de una metasentencia. La misma puede entederse como una macroexpansión que se reemplaza
por:
int i 0
while i < jAj
:?! 0  i  jAj ^
8k = 0  k < i : postsbi 7! kc ^
8k = i  k < jAj : A[k] = A@pre[k]
:# jAj i
do
s
i i+ 1
od
Donde posts = post(s; 0  i < jAj ^ Cl9fAg(p)). Se le realiza una sustitución de i por k porque se
la utiliza para expresar que todos los elementos ya visitados (indexados con k) satisfacen que s ha sido
aplicado sobre ellos.
Una vez definida la metasentencia map, se puede utilizar para escribir de forma más compacta y
legible los programas anteriores.
1: easyArrayInc(A)
2: :? jAj > 0
3: :! 8k = 0  k < jAj : A[k] = A@pre[k] + 1
4: {
5: map
6: A[i] A[i] + 1
7: in A[.. i ..]
8: }
Incrementar un arreglo en 1 usando map
55

1: easyFirstN(A)
2: :? jAj > 0
3: :! 8k = 0  k < jAj : A[k] = k
4: {
5: map
6: A[i] i
7: in A[.. i ..]
8: }
Lista de los primeros naturales usando map
Con un esquema como este ya no es necesario proveer invariante para un número importante de
casos. Observar cómo desaparece el engorroso invariante que acompañaba de forma necesaria a estos
programas.
4.2. Metasentencia find
Otra tarea que aparece con cierta frecuencia al escribir programas es encontrar el primer elemento
de un arreglo que satisface una determinada propiedad. Observar los siguientes ejemplos:
1: linearSearch(A; e; i)
2: :? 8k = 0  k < jAj : A[k] = e
3: :! A[i] = e ^ A = A@pre ^ e = e@pre
4: {
5: i 1
6: int j 0
7: while j < jAj ^ i = 1
8: :?! 0  j  jAj ^
9: (i = 1 ) 8k = 0  k < j : (A[k] 6= e)) ^
10: (i 6= 1 ) 8k = 0  k < i : (A[k] 6= e) ^ a[i] = e) ^
11: A = A@pre ^ e = e@pre
12: :# jAj j
13: do
14: if A[j] = e then
15: i j
16: fi
17: j j + 1
18: od
19: }
Busqueda lineal
56

El invariante I se obtiene a partir de la postcondición del ciclo Qc de la siguiente forma:
I
def
= l  i  h ^ Qcbh 7! ic
Se incorporan las cotas de la variable i; tal información nunca podría venir de Qc ya que i es una variable
local al for.
Resta indicar la forma en la que se calcula la postcondición Qc para el for. Si s es una sentencia
en donde se encuentra el for que quiere reemplazarse y q es la postcondición a la que s debe llegar, se
utiliza forQ(s; q) para obtener la postcondición Qc del for dentro de s para llegar a q. Se define de la
siguiente manera:
forQ(for i from l to h do s od; q)
def
= q
forQ(s1 s2; q)
def
=
(
forQ(s2; q) si for i from l to h do s od 2 s2
forQ(s1; pre(s2; q)) sino
forQ(if g then s1 else s2 fi; q)
def
=
(
forQ(s1; q) si for i from l to h do s od 2 s1
forQ(s2; q) sino
forQ(while g :?! inv :# var do s od; q)
def
= forQ(s; q)
Con la nueva metasentencia for, podemos reescribir el programa que calcula el máximo de un arreglo
de la siguiente manera:
1: easyMax(A;m)
2: :? jAj > 0
3: :! 8k = 0  k < jAj : m  A[k] ^
4: 9k = 0  k < jAj : m = A[k] ^ A = A@pre
5: {
6: m A[0]
7: for i from 1 to jAj do
8: if A[i] > m then
9: m A[i]
10: fi
11: od
12: }
El máximo de un arreglo usando for
Recordar que en el caso de una metasentencia for la inferencia de invariante se realiza sin obedecer
a ningún patrón de iteración. Sin embargo, el candidato a invariante que se obtiene puede ser incorrecto
o insuficiente para poder probar la corrección del ciclo.
Esto no supone problema alguno para el proceso de verificación. El candidato a invariante obtenido
mediante la técnica de inferencia presentada es utilizado para ver si alcanza a probar la corrección del
ciclo. Se espera que esto sea así la mayoría de las veces, pero si se fallara para probar esta propiedad
ya sea porque el invariante es muy débil, o porque las herramientas de prueba no alcanzan a probarlo
hay algunas opciones a tener en cuenta.
61

Capítulo 5
Implementación
In seeking absolute truth we aim at the unattainable and must be content with broken portions."
William Osler
En los capítulos anteriores propusimos un lenguaje de programación muy simple, cuyo diseño obe-
dece principalmente a la meta de facilitar la verificabilidad de sus programas. Presentamos técnicas y
conceptos que permiten demostrar formalmente la corrección y terminación de programas escritos en
este lenguaje. Para poder determinar de forma automática si un programa es seguro (es correcto y
termina) es necesario contar con una herramienta que implemente estas técnicas.
Recordar que para que un programa sea seguro debe suceder que todos sus procedimientos
proc(p1; : : : ; pk) :? pre :! post f s g cumplan:
fpreg s fpostg
Una forma muy simple de corroborar este hecho es:
Implementar un algoritmo que use algún tipo de oráculo para calcular Q = post(s; pre).
Preguntarle a dicho oráculo si Q j= post.
Si no se toman ciertas precauciones dicho enfoque tiene un serio inconveniente: el tamaño de las
preguntas que se le hacen al oráculo puede crecer exponencialmente respecto a la entrada. Como ejemplo
suponer que se cuenta con la siguiente sentencia s:
if x > 0 then
x x+ 1
else
x x+ 2
fi
En ese caso:
post(s; x = 7) = 9 x0 : Int (x0 = 7 ^ x0 > 0 ^ x = x0+1) _ 9 x0 : Int (x0 = 7 ^ x0  0 ^ x = x0+2)
Si en cambio se secuencia s dos veces consecutivas, luego:
post(s s; x = 7) = 9 x00 : Int ((post(s; x = 7))bx 7! x00c ^ x00 > 0 ^ x = x00 + 1) _
63

9 x00 : Int ((post(s; x = 7))bx 7! x00c ^ x00  0 ^ x = x00 + 2)
Observar que post(s s; x = 7) contiene a post(s; x = 7) dos veces. Si se hiciera post(s s s; x = 7) tal
subexpresión aparecería 4 veces. Se puede apreciar el crecimiento exponencial con respecto a la cantidad
de condicionales que aparecen en el código (aun cuando estos no están anidados). Este crecimiento
exponencial indica que un enfoque ingenuo (calcular la postcondición del cuerpo y ver que implica el
contrato) no es eficiente. Se trata de un hecho conocido en el ámbito de la verificación.
A continuación analizamos el funcionamiento de una de las herramientas que representa el estado
del arte, Spec# [BLS04]. Algunos aspectos de nuestro enfoque están inspirados en esta herramienta,
aunque con una serie de diferencias importantes. Estos puntos de contacto, así como las cuestiones en
las cuales nuestro enfoque se aparta, serán detallados en la Subsección 5.1.1.
La metodología usada por la herramienta Spec# es traducir programas en un dialecto de C# a un
lenguaje intermedio denominado Boogie-PL [DL05]. Esta traducción es realizada de tal forma que si
el programa traducido es correcto luego el programa original también lo es.
El lenguaje intermedio Boogie-PL tiene una semántica no determinística y no está pensado para
que sus programas sean ejecutados sino para especificar, mediante una abstracción, las características
que cumplen todas las trazas de un programa en el lenguaje original.
Al contar con un lenguaje intermedio, la verificación puede desdoblarse en dos problemas:
1. Traducir programas escritos en cualquier lenguaje imperativo a programas del lenguaje inter-
medio que describen todas las trazas posibles. La traducción tiene que ser tal que preserve la
corrección de la verificación que se hará sobre ella respecto de la corrección del programa original.
Esto presenta inconvenientes tales como describir en el lenguaje intermedio el efecto de las asig-
naciones, de los ciclos, los condicionales y las características de objetos como dynamic binding. En
el caso particular de Boogie-PL existen traducciones desde Spec# y desde C [CLQR07].
2. Verificar que todas las trazas descriptas en la traducción hecha en el punto anterior satisfacen
todos los contratos. Para ello se utilizan herramientas de demostración automática o asistida.
El lenguaje Boogie-PL fue diseñado teniendo en cuenta este segundo punto. Un programa
Boogie-PL se puede traducir de forma lineal para obtener un problema que una herramienta
de verificación puede tratar [BL05].
Los principales comandos
1
de Boogie-PL son:
assume f
Este comando indica que todas las trazas del programa satisfacen f .
assert f
Este comando indica que todas las trazas del programa deberían satisfacer f . Es utilizado para
verificar que el programa original cumple con todos sus contratos.
c1  c2
Se trata de la decisión no determinística entre los comandos c1 y c2. Una traza puede seguir
cualquiera de los dos caminos.
c1 c2
El secuenciamiento de los comandos c1 y c2.
1
Llamaremos comando a cualquier instrucción de un lenguaje intermedio cuyo fin es la verificación de programas.
64

havoc(v)
Este comando asigna de forma no determinística un valor cualquiera a la variable v.
La herramienta Spec# traduce las asignaciones siguiendo un esquema dynamic single assignment o
DSA. El mismo utiliza encarnaciones, las cuales pueden entenderse como fotografías del valor que tiene
una variable en un determinado punto del programa. Cada vez que se asigna un valor a una variable se
crea una nueva encarnación para la misma.
Por ejemplo, el siguiente fragmento de un programa:
a = 15;
a = a+ 10;
a = a  25;
Se traduce de la siguiente forma:
assume a0 = 15
assume a1 = a0 + 10
assume a2 = a1  25
Un condicional de la siguiente forma:
if(g) s1 else s2
Se traduce del siguiente modo:
(assume g c1)  (assume :g c2)
Donde c1 y c2 son las traducciones de s1 y s2 respectivamente.
Un ciclo:
while(i > 0) invariant(i >= 0) i;
Se traduce de la siguiente forma:
assert i >= 0
assume ic >= 0
(assume ic > 0 assume i
0
c = ic 1 assert i
0
c >= 0 assume false)  assume ic <= 0
En general un ciclo se traduce utilizando una encarnación fresca para cada una de las variables que
es modificada por el mismo. Por otra parte se utiliza el operador de decisión no determinística para
describir que en una traza la ejecución puede realizar una iteración o puede dejar de iterar. En caso de
producirse una iteración genérica, la misma debe preservar el invariante sobre las encarnaciones de las
variables al finalizar.
Tal como mencionamos en el Capítulo 1, la herramienta Spec# no verifica terminación, por lo
tanto no se preocupa por el decrecimiento de una función variante. Sólo comprueba que todas las
ejecuciones que terminan sean correctas. Nuestra herramienta, en cambio, debe proveer una verificación
más específica al garantizar que todas las ejecuciones terminan y son correctas.
Los llamados a métodos se traducen incorporando un assert de su precondición y un assume de su
postcondición. Por el contrario las definiciones de métodos son traducidas incorporando antes del cuerpo
un assume con la precondición y agregando al final un assert con la postcondición.
65

En general, los comandos havoc(v) que asigna no determinísticamente un valor a la variable v no
son necesarios como parte del lenguaje intermedio. El esquema de traducción DSA puede simplemente
incorporar una encarnación fresca para v sobre la cual no se conoce absoultamente nada.
Una vez traducido todo el programa se obtiene una gran secuencia de comandos de Boogie-PL que
describe todas las posibles trazas que el mismo puede tomar. Si ninguno de los asserts de la traducción es
violado, luego ninguna ejecución del programa original violará contrato alguno. Eso significa que todos
los contratos explícitos (tales como postcondiciones e invariantes) serán cumplidos y adicionalmente no
se harán accesos fuera de rango, divisiones por cero u otros requerimientos implícitos.
La ventaja de utilizar un lenguaje intermedio de las características de Boogie-PL, cuyos comandos
no tienen efectos secundarios y utiliza un mecanismo de DSA es que se evita el problema de la explosión
exponencial. Esto se debe a que existe una forma en la que se puede calcular la weakest precondition de
una secuencia de comandos de forma lineal [BL05]. Se trata básicamente de seguir las siguientes reglas:
wp(assume p; q)
def
= p) q
wp(assert p; q)
def
= p ^ q
wp(c1  c2; q)
def
= wp(c1; q) ^ wp(c2; q)
wp(c1 c2; q)
def
= wp(c1; wp(c2; q))
La weakest precondition de la traducción del programa es una fórmula cuya validez lógica implica
que ningún assert es violado. Por ende para ver que un programa no viola ninguno de sus contratos
alcanza con demostrar que esta fórmula es teorema bajo las teorías de los arreglos, enteros, reales, etc.
En el caso de Spec# este problema es resuelto utilizando un demostrador automático llamado Z3, el
cual pertenece a una clase de programas denominados demostradores de satisfactibilidad módulo teorías
o SMT solvers. Se trata de herramientas muy difundidas en el mundo de la verificación de hardware,
aunque crecientemente se las ha encontrado muy útiles para verificar software [BdMS05].
En el caso general, una instancia del problema de la satisfactibilidad módulo teorías puede ser vista
como una fórmula en lógica de primer orden en la cual ciertos predicados y símbolos de función tienen
una interpretación basada en una serie de teorías de primer orden con igualdad como por ejemplo los
enteros, los reales, los arreglos, etc.
Un SMT solver abstrae los predicados y los reemplaza por variables booleanas. De esta forma el
problema se convierte en una instancia que puede ser resuelta por un SAT solver. Una vez obtenidos
cuáles de los predicados abstraídos deben ser verdaderos para satisfacer la fórmula, el SMT solver
procede a ver si tal combinación es consistente. Para ello utiliza módulos que interpretan cada una de
las teorías que el solver incorpora. Combinando los diversos módulos establece si los predicados que
deben ser verdaderos suponen una contradicción. De ser así se busca otra combinación de predicados,
caso contrario la fórmula es satisfacible.
Las expresiones que este tipo de herramientas atacan involucran teorías que son, muchas veces,
indecidibles (como por ejemplo aritmética de Peano) y por ende se debe contemplar desconocido como
una respuesta posible. En definitiva la salida puede tomar una de tres formas:
1. La herramienta pudo demostrar que la fórmula es satisfacible.
2. La herramienta pudo demostrar que la fórmula es insatisfacible.
3. La herramienta no pudo demostrar ninguno de los dos casos anteriores.
66

Debido a que se busca probar que la wp de la traducción del programa es válida, se le pregunta a Z3
si su negación es insatisfacible. En caso de que lo sea, el programa no viola ninguno de sus contratos. En
caso de que no lo sea, Spec# utiliza diversos mecanismos para rastrear qué parte de la fórmula no pudo
ser probada y relacionar dicho problema con un punto del programa para notificar al programador.
Un problema de este enfoque monolítico es que no permite ser mejorado en cuanto a la posibilidad
de incorporar diversos demostradores. Incluso atacando la única fórmula con diversos SMT solvers
podría suceder que la misma no sea demostrable ya que diversos fragmentos de la misma hacen fracasar
a distintos demostradores.
En definitiva, este enfoque fuerza que cada solver sepa manejar todas las teorías mencionadas en la
fórmula. Mientras que en la práctica, en general, cada demostrador maneja sólo algunas de ellas.
El resto de este capítulo se divide en tres partes. En la primera de ellas presentamos un enfoque al-
ternativo de traducción y posterior verificación. El mismo explota las características de nuestro lenguaje
para permitir la combinación modular de diversos SMT solvers sobre fragmentos a verificar.
En la segunda parte brindamos una breve explicación acerca del prototipo de herramienta que
implementamos como parte de este trabajo. Comentamos sus principales características y marcamos
algunas consideraciones sobre su sintaxis concreta.
En la tercera y última parte analizamos el comportamiento del prototipo que implementamos. Se
prueba su desempeño sobre algunos ejemplos que permiten apreciar sus capacidades y limitaciones.
5.1. Un enfoque modular para la verificación
La verificación de programas a través de un lenguaje intermedio tiene la ventaja de evitar la explosión
combinatoria que se da al calcular las postcondiciones, tal como se vio al comienzo de este capítulo.
Sin embargo el enfoque monolítico adoptado por Spec# genera una única wp para todo un programa
y luego la ataca con un único SMT solver.
Como primera mejora pensamos en utilizar diversos demostradores para atacar dicha fórmula. Esto
en principio podría ser positivo, ya que existen diversos SMT solvers desarrollados por universidades,
grupos de investigación o empresas. Cada uno de ellos tiene implementadas distintas reglas que los hacen
comportarse mejor o peor que el resto según la fórmula que se esté probando. Existen problemas que
son resueltos muy rápidamente por alguna de estas herramientas, mientras que otras no pueden o se les
hace muy difícil tratarlos.
A modo de ejemplo, suponer que se cuenta con un demostrador que funciona bien con fórmulas que
prediquen sobre arreglos y se tiene otro demostrador que funciona bien con fórmulas aritméticas. En ese
caso se puede utilizar el demostrador adecuado según el problema que presente la fórmula a tratar. En
caso de que una fórmula contenga problemas de arreglos y de aritmética no habría forma de tratarla con
ninguno de los dos demostradores. Sin embargo, con una partición conveniente de la misma, se podría
alimentar a cada uno de los demostradores con el fragmento sobre el que trabaja mejor.
Con esta intuición en mente, decidimos que valía la pena buscar un enfoque que permita encarar la
verificación de forma gradual. Al atacar la fórmula parte por parte se puede combinar la potencia de
diversos demostradores aprovechando los puntos fuertes de cada uno de ellos.
Suponiendo que se pudiera partir el problema de la verificación en pequeñas instancias de verificación
más pequeñas, luego se puede utilizar un oráculo compuesto por diversos SMT solvers para atacar
cada una de ellas. El oráculo puede ser visto como una interfaz abstracta hacia un orquestador que le
realiza una pregunta a cada uno de los solvers. Ante la primer respuesta definitoria o sea, distinta de
67

Donde cmd(s1; D) = (c1; D1) y cmd(s2; D) = (c2; D2). Se utiliza V 0 para dar encarnaciones nuevas
a todas las variables modificadas por alguna de las dos ramas
3
, identificado por el conjunto V , definido
de la siguiente forma:
V
def
= fv j D1(v) 6= D2(v)g
Ante un condicional aparece el requisito de que la guarda sea una expresión booleana segura. Por otra
parte se genera un comando condicional que al final de cada rama tiene un binding entre el último valor
de las variables en la misma con respecto al valor de las variables luego del condicional según el mapeo
resultante.
cmd(while g :?! inv :# var do s od; D)
def
=

verify safeB(D(inv) ^D(g)) ^ safeI(D(var))
verify D(inv)
lemma
assume M(inv) ^M(g)
verify safeB(M(inv) ^M(g)) ^ safeI(M(var))
verify M(var) > 0
c
verify M 0(inv)
verify M 0(var) < M(var)
assume D0(inv) ^ :D0(g)
; D0

Donde M = DfV 7! V 0g con V = modVars(s). Por otra parte cmd(s; M) = (c;M 0). Y finalmente
D0 = DfV 7! V 00g.
Se asume como conocido el invariante sobre un mapeo de variables genérico y se incorpora un verify
por cada una de las premisas de la regla para la semántica abstracta.
El mapeo de variables resultante de la traducción de un ciclo únicamente tiene encarnaciones nuevas
para aquellas variables que fueron potencialmente modificadas por una iteración genérica. El resto de
las variables conserva sus encarnaciones previas al ciclo por ende toda la información que se conocía
sobre ellas es preservada. De esta manera se está trabajando como si se hubiera fortalecido el invariante
del ciclo ampliándolo para preservar la información conocida sobre las variables que el ciclo no modifica,
tal como se presentó en la Subsección 3.5.2.
cmd(call proc(cp1; : : : ; cpk); D)
def
=

verify D(Pprocbpi 7! cpic)
assume D0(Qprocbpi 7! cpic)
; D0

Donde D0 = Dfpi 7! p0ig
3
Se comete un abuso de notación al realizar un assume sobre muchas variables a la vez. Esto puede verse como syntactic
sugar que se reemplaza por un assume para cada una de las variables en V . De forma similar se extiende naturalmente el
concepto de mapeo de variables aplicado a un conjunto V .
70

Traducción de la metasentencia find
De manera similar, traducimos la metasentencia find directamente sobre el lenguaje intermedio. De
esta forma evitamos agregar las verificaciones de que el invariante vale al comienzo y se preserva, el
variante es positivo y decrece; todas estas verificaciones son innecesarias ya que la forma en que se
construyen hace que siempre sean correctas.
La traducción para un find, evitando realizar las verificaciones que siempre serían correctas, es:
cmd(i find x as s in A[.. j ..]; D)
def
=

lemma
assume 0  j < jAj
c
assume
(i0 6= 1) 8k = 0  k < i0 : :postsbj 7! kc ^ postsbj 7! i
0c)
^ (i0 = 1) 8k = 0  k < jAj : :postsbj 7! kc)
; Dfi 7! i0g

Donde cmd(s; Dfj 7! j0g) = (c;M)
De forma similar a la traducción de la metasentencia map, en este caso no se utiliza el mapeo M ya
que se conoce por construcción que el invariante inferido es preservado.
Traducción de la metasentencia for
El caso de la metasentencia for es ligeramente distinto a las dos traducciones mencionadas. Tal
como se presentó en el capítulo anterior, para traducir una metasentencia for es necesario contar con un
candidato a invariante. El mismo no obedece a ningún patrón particular, por el contrario es obtenido a
partir de una transformación de la postcondición del for, la cual llamamos Qc.
Tal como mencionamos en la Sección 4.3, para obtener una postcondición Qc nuestro enfoque es
comenzar desde el final del procedimiento tomando la postcondición del contrato. A partir de allí se
sube aplicando el cálculo de precondiciones hasta llegar al punto final de la metasentencia for que se
desea traducir.
Sin embargo, el cálculo de precondiciones presenta el mismo problema de explosión exponencial que
el cálculo de postcondiciones. Si se siguiera directamente la definición dada en el capítulo anterior se
obtendría un invariante exponencialmente grande respecto de la distancia que separa la metasentencia
for del final de procedimiento.
El lenguaje intermedio se introdujo como un medio para poder obtener precondiciones y postcondi-
ciones de forma eficiente. Por lo tanto si se pudiera trabajar con la traducción al lenguaje intermedio
de la cola del procedimiento (es decir, el fragmento que va desde el final del for hasta el final del
procedimiento) luego se podría calcular su precondición de forma eficiente.
Se produce una situación de dependencia circular. Para poder traducir un for es necesario su invarian-
te. Su invariante depende de la postcondición deseada Qc. Esta postcondición depende de la traducción
de la cola del procedimiento. La traducción de la cola del procedimiento no puede ser obtenida hasta
no traducir el for.
Presentamos a continuación un ejemplo que muestra la forma en la que resolvimos este problema.
Contamos con el siguiente procedimiento que calcula el mínimo de un arreglo:
73

1: easyMin(A;m)
2: :? jAj > 0
3: :! 8k = 0  k < jAj : m  A[k]
4: {
5: int min A[0]
6: for i from 1 to jAj do
7: if A[i] < min then
8: min A[i]
9: fi
10: od
11: m min
12: }
El mínimo de un arreglo usando for
Para poder traducir la metasentencia for que aparece en el procedimiento es necesario obtener la
postcondición deseada. Sin embargo, en una primera pasada no se traduce el for. Lo que obtenemos no
es un plan de demostración, sino un protoplan de demostración en el cual todavía permanecen elementos
ajenos al lenguaje intermedio.
En el caso del ejemplo se obtendría:
assume jAj > 0
assume min0 = A[0]
for i in [1; jAj)
case A[i] < minf in assume min0f = A[i] and skip
assume m0 = minl
verify 8k = 0  k < jAj : m0  A[k]
Observar la tercera línea, en la cual aparece un elemento for, ajeno al lenguaje intermedio de planes de
demostración. Se trata de un protoplan de demostración.
A partir de este punto se puede realizar una segunda pasada, en la cual se parte desde el final del
protoplan y se recorre hacia arriba obteniendo precondiciones hasta el punto en el que se encuentra
algún elemento ajeno al lenguaje intermedio.
En el caso del ejemplo se llega hasta el for habiendo acumulado:
8k = 0  k < jAj : minl  A[k]
Observar que con respecto al último verify, la encarnación m0 es reemplazada por minl gracias al
comando assume m0 = minl.
Utilizando esta postcondición deseada para el for Qc se puede obtener el siguiente invariante:
8k = 0  k < i : min  A[k]
Una vez que se tiene el invariante se puede convertir el elemento for ajeno al lenguaje intermedio.
Obtenidos los comandos correspondientes a tal traducción se puede calcular una precondición de los
mismos y proseguir hacia arriba. Se repite este procedimiento hasta quitar todos los elementos ajenos
al lenguaje intermedio para obtener un plan de demostración que pueda ser verificado utilizando el
algoritmo follow.
74

Las metasentencias map y find tienen parámetros adicionales que indican los límites inferior y
superior de iteración. Esto permite recorrer un subarreglo, aumentando la expresividad de estos
comandos. Adicionalmente, la metasentencia find permite recorrer desde atrás hacia adelante.
La sintaxis concreta para map es:
map e in A[l::i::h] fsg
La variable e sirve como binding para referirse a A[i] dentro de s. La variable i itera entre l y h
inclusive y estas cotas deben estar en rango.
La sintaxis concreta para find es:
i nd rst v in A[l::j::h] fsg
Se itera usando la variable j empezando en l y avanzando hasta llegar a h. Se deja en i el primer
valor de j que haga que s asigne un valor distinto de 0 a la variable v. Reemplazando rst por
last se itera hacia atrás.
Los tipos de los parámetros formales de un procedimiento deben ser especificados de manera
manual sin embargo podría implementarse un algoritmo que los infiera.
Mostramos el siguiente ejemplo para presentar la sintaxis concreta para definir procedimientos:
name(p1; p2[]; : : : ; pk) :? pre :! post :  pi1 ; : : : ; pim fsg
Se sufija el nombre de un parámetro formal con [] en su definición para indicar que se trata de
un parámetro de tipo arreglo. Por otra parte observar que la definición incluye una cláusula : 
que indica cuáles de los parámetros formales son modificables. Si un parámetro formal p no es
declarado como modificable luego se verifica que nunca sea asignado en el cuerpo del procedimiento
y se agrega p = p@pre a la postcondición.
Aparte de la sintaxis, la otra diferencia entre las definiciones formales presentadas hasta aquí y el
prototipo implementado son los chequeos de expresiones seguras. En la versión con la que contamos
al momento de la confección de este documento aún no se encuentra implementada la generación de
planes de prueba que incluyan chequeos de expresiones seguras. La ausencia de esta característica no
nos pareció crítica a la hora de desarrollar una herramienta que sirva como prueba de concepto para
llevar a la práctica nuestras ideas.
Una característica del prototipo que es digna de ser remarcada es la utilización del patrón de diseño
visitor [PJ98]. El mismo permite la definición de operaciones sobre objetos en una estructura de clases sin
necesidad de alterar el código de las mismas. Tiene una forma de funcionamiento que podría compararse
con la definición de funciones por pattern matching en el paradigma funcional.
Haciendo uso de la herencia y el patrón visitor, el prototipo permite ser fácilmente extendido con
nuevas metasentencias, nuevos demostradores automáticos, etc.
5.3. Casos de prueba
Antes de introducir los casos de prueba, es preciso mencionar que por una cuestión de consistencia,
en su presentación se optó por preservar la sintaxis con la que se trabajó toda la tesis.
El primer caso se trata de un programa que no hace uso de ninguna metasentencia, sin embargo
es de interés por tratarse de un algoritmo de ordenamiento clásico. Los invariantes son complejos, con
79

cuantificaciones doblemente anidadas, por lo tanto se espera que se trate de un caso interesante de
verificar.
1: bubbleSort(A)
2: :? jAj > 0 ^ . arreglo no vacío
3: 8i1 = 0  i1 < jAj : 8i2 = 0  i2 < jAj : i1 6= i2 ) A[i1] 6= A[i2] . sin repetidos
4: :! 8k = 0  k < jAj 1 : A[k] < A[k + 1] ^ . ordenado
5: 8i1 = 0  i1 < jAj : 9i2 = 0  i2 < jAj : A[i1] = A@pre[i2] . permutación
6: {
7: int i jAj 1
8: while i > 0
9: :?! 0  i  jAj 1 ^
10: 8k = i  k < jAj 1 : A[k]  A[k + 1] ^ . parcialmente ordenado
11: 8n = 0  n  i : 8k = i < k < jAj : A[n]  A[k] ^ . i separa mayores y menores
12: 8i1 = 0  i1 < jAj : 8i2 = 0  i2 < jAj : i1 6= i2 ) A[i1] 6= A[i2] ^ . sin repetidos
13: 8i1 = 0  i1 < jAj : 9i2 = 0  i2 < jAj : A[i1] = A@pre[i2] . permutación
14: :# i
15: do
16: int j 0
17: while j < i
18: :?! 0  i  jAj 1 ^
19: 8k = i  k < jAj 1 : A[k]  A[k + 1] ^
20: 8n = 0  n  i : 8k = i < k < jAj : A[n]  A[k] ^
21: 8i1 = 0  i1 < jAj : 8i2 = 0  i2 < jAj : i1 6= i2 ) A[i1] 6= A[i2] ^
22: 8i1 = 0  i1 < jAj : 9i2 = 0  i2 < jAj : A[i1] = A@pre[i2] ^ . I de afuera
23: 0  j  i ^
24: 8k = 0  k < j : A[k]  A[j] . j-ésimo mayor a su izquierda
25: :# i j
26: do
27: if A[j] > A[j + 1] then
28: int j1 j + 1
29: call swap(A; j; j1)
30: fi
31: j j + 1
32: od
33: i i 1
34: od
35: }
36: swap(A; i; j)
37: :? 0  i < jAj ^ 0  j < jAj
38: :! 8k = 0  k < jAj : k 6= i^k 6= j ) A[k] = A@pre[k] ^A[i] = A@pre[j] ^A[j] = A@pre[i]
39: {
40: int tmp A[i]
41: A[i] j
42: A[j] tmp
43: }
Algoritmo de ordenamiento bubble sort
80

Observar que se requiere que todos los elementos del arreglo sea distintos y se garantiza que el
resultado es una permutación ordenada del arreglo original. Idealmente nos gustaría poder verificar un
programa que contemple la aparición de repetidos, sin embargo se necesitarían predicados de especi-
ficación que puedan expresar la cantidad de apariciones para poder establecer adecuadamente que el
resultado es una permutación.
El contrato del procedimiento principal no refleja detalles de implementación, por el contrario,
especifica el comportamiento esperado. Por otra parte, los invariantes responden a la forma particular
en la que implementamos el algoritmo de ordenamiento. Esta diferencia conceptual entre qué y cómo
es resuelta gracias a la capacidad deductiva de los demostradores.
Este programa genera 45 preguntas que se le realizan al oráculo. La gran mayoría de ellas es respon-
dida por el demostrador Yices, sin embargo una es resuelta únicamente por Z3. De no haber utilizado
los demostradores en paralelo este sería un caso que no se podría atacar.
El tiempo de ejecución es de aproximadamente 4 segundos en una computadora Pentium IV de
2800 MHz con 1 GB de memoria RAM.
Presentamos a continuación un ejemplo que involucra la metasentencia for y anotaciones con arit-
mética no lineal. Esto supone un reto más que interesante ya que la gran mayoría de los demostradores
automáticos no soportan este tipo de aritmética. Sin embargo, CVC3 tiene cierto soporte muy limitado
de aritmética no lineal que permite resolver algunas cuestiones.
1: sumFirstN(n; s)
2: :? n > 0
3: :! s = n  (n 1)=2 ^ n = n@pre
4: {
5: s 0
6: for i from 1 to n do
7: s s+ i
8: od
9: }
Suma de los primeros n 1 naturales
El invariante inferido en este caso es:
1  i  n ^ s = i  (i 1) ^ n = n@pre
Este programa genera un total de 3 preguntas al oráculo, de las cuales 2 son respondidas por Yices
y una de ellas, que representa la preservación del invariante y por ende contiene no linearidad, es
respondida por CVC3.
El tiempo de ejecución en este caso es despreciable.
Por último, mostramos un ejemplo donde se pueden apreciar algunas de las limitaciones del enfoque
de verifiación automática usando demostradores de teoremas. En este caso se trata de un procedimiento
para determinar si un arreglo se encuentra ordenado.
81

Capítulo 6
Conclusiones y trabajo a futuro
La música empieza donde se acaba el lenguaje."
E.T.A. Hoffmann
6.1. Conclusiones
Partimos en este trabajo de la hipótesis de que las herramientas de verificación automática más
difundidas en la actualidad tienen ciertos inconvenientes propios de la forma en la que son concebidas
como adiciones a un lenguaje preexistente y complejo.
Inspirados en este sentido nos planteamos el objetivo de explorar el potencial de trabajar con ve-
rificadores y lenguajes de programación concebidos a la par. Para ello propusimos un lenguaje de pro-
gramación muy básico, pero cuyas metas de diseño y sus características fueron establecidas teniendo en
cuenta la verificabilidad.
Dotamos a este lenguaje de un sistema de tipos extendido que captura la noción de corrección y
terminación de programas mediante el uso de un oráculo. Propusimos técnicas que, basadas en este
sistema de tipos, infieren una precondición o una postcondición para un fragmento de un programa.
Con estas herramientas nos dedicamos a ampliar el lenguaje con mecanismos que permiten ahorrar
la tarea de escribir ciertas anotaciones para la verificación. En este sentido propusimos la inferencia de
anotaciones de procedimientos, el refuerzo de invariantes y las metasentencias. Estas últimas combinan
una estructura de iteración conocida y frecuente con las técnicas de inferencia para obtener buenos
candidatos a invariantes.
Para complementar el trabajo teórico realizado implementamos un prototipo de herramienta verifi-
cadora que lleva a la práctica una gran parte de las ideas propuestas. Esta herramienta aplica una serie
de reducciones sintácticas a las fórmulas y combina diversos demostradores automáticos de forma tal
de obtener mejores resultados.
A partir del trabajo realizado podemos concluir que efectivamente el hecho de diseñar un lenguaje al
mismo tiempo que su framework de verificación permite avanzar en ciertas líneas que de otra manera no
serían posibles. Al concebir una herramienta verificadora para un lenguaje preexistente se busca realizar
la menor cantidad de modificaciones posibles al mismo. Un enfoque de ese tipo jamás podría aprovechar
las ventajas de ampliar el lenguaje con construcciones de alto nivel como las presentadas en nuestro
trabajo.
Por otra parte, al trabajar con un lenguaje core muy simple, el desarrollo de técnicas de inferencia
83

Apéndice A
Demostraciones
A.1. Demostración del Teorema 3.1
Sean i 2 IntExp; A 2 ArrayExp; b 2 BoolExp. Sea  2 M, luego:
si JsafeI(i)KBool = true luego existe algún n 2 Z : JiK
Int
 = n
si JsafeA(A)KBool = true luego existe algún A 2 A : JAK
Array
 = A
si JsafeB(b)KBool = true luego existe algún x 2 ftrue; falseg : JbK
Bool
 = x
Dem:
Inducción estructural en i 2 IntExp; A 2 ArrayExp; b 2 BoolExp.
Caso expresión entera atómica i = v; i = v@pre; i = n.
Sus reglas para semántica no tienen hipótesis, con lo cual siempre existe un n 2 Z tal que JiKInt =
n.
Caso tamaño de un arrreglo i = jAj.
Observar que safeI(jAj) pide safeA(A), por lo tanto si la primera es verdad también lo es la segunda.
Si safeA(A) es verdad luego por hipótesis inductiva vale que A tiene su valor definido. Por ende
se le puede dar valor a jAj.
Caso acceso a un arreglo i = A[i].
Las reglas para semántica en estos casos exigen que:
1. El arreglo esté definido: JAKArray = A.
2. El índice esté definido: JiKInt = n.
3. El índice esté en rango: 0  n <

A


.
Observar que safeI(A[i]) pide que safeA(A) y que safeI(i). Luego se puede aplicar la hipótesis
inductiva para obtener las primeras dos condiciones.
La tercera condición es satisfecha por la última parte de safeI(A[i]), la cual pide que 0  i < jAj.
Recordar que JjAjKInt =

A


si JAKArray = A.
86

A.3. Demostración del Teorema 3.2
Sea un programa seguro  y sea p un procedimiento en . Luego:
para toda valuación  2 Mp sucede que si JP( p)K
Bool
 = true luego existe una valuación 
0 2 Mp
tal que  .  : p . 0 y JQ( p)K
Bool
0 = true
Dem:
El caso en que  sea ; es trivial, ya que no existe un procedimiento p tal que p 2 ;.
Suponiendo que  es seguro, entonces se le agrega un nuevo procedimiento:
proc(p1; : : : ; pk) :? pre :! post f m1; : : : ;mn gs
Tal que fpreg s fpostg.
Una ejecución de  extendido con proc que comienza desde el procedimiento p cumple uno de los
siguientes dos escenarios:
1. p 2  en cuyo caso aplicando la hipótesis inductiva se sabe que la propiedad vale.
2. p es el procedimiento recién agregado, proc. Hay que demostrar que cualquier valuación que
satisface pre, puede ejecutar el cuerpo s y llegar a otra valuación que satisface post. Se analizará
este caso en detalle.
Se sabe que fpreg s fpostg, se hará inducción en las demostraciones que permiten llegar a tal juicio:
Caso asignación a una variable entera:
p j= safeI(i) 9 v0 : Int (pbv 7! v0c ^ v = ibv 7! v0c) j= q
A-SENT-IASSIGN
fpg v i fqg
Suponiendo p j= safeI(i), a partir del Teorema 3.1, se sabe que existe un n 2 Z : JiKInt = n.
Con lo cual, se cumple la hipótesis de la regla S-SENT-IASSIGN, la cual permite afirmar que:
 . v i . fv 7! ng
Falta ver que JqKBoolfv 7!ng, pero como 9 v
0 : Int (pbv 7! v0c ^ v = ibv 7! v0c) j= q basta ver que:
J9 v0 : Int (pbv 7! v0c ^ v = ibv 7! v0c)KBoolfv 7!ng = true
Lo cual es válido si hay algún valor entero para v0 que haga válido a:
pbv 7! v0c ^ v = ibv 7! v0c
Tal valor es v0 = (v), o sea, el valor de v antes de la asignación. Con lo cual la fórmula que debe
ser válida bajo fv 7! ng es:
pbv 7! (v)c ^ v = ibv 7! (v)c
90

Caso sentencia vacía:
p j= q
A-SENT-SKIP
fpg skip fqg
Sin necesidad de hipótesis, se puede aplicar la regla S-SENT-SKIP, la cual permite afirmar que:
 . skip . 
Resta verificar que toda valuación  2 M tal que cumple que JpKBool = true cumple también
que JqKBool = true, lo cual es precisamente la definición de p j= q, lo cual se sabe que se cumple
ya que es una hipótesis de la regla.
Caso secuenciamiento:
fpg s1 frg frg s2 fqg
A-SENT-SEQ
fpg s1 s2 fqg
Suponiendo las hipótesis de la regla, por hipótesis inductiva, para toda valuación  2 M tal que
JpKBool = true, vale que  . s1 . 
0
y JrKBool0 = true.
Por otra parte, y también usando la hipótesis inductiva, como 0 es tal que JrKBool0 = true, luego
vale que 0 . s2 . 00 y JqKBool00 = true.
Por lo tanto, se tienen las hipótesis suficientes para aplicar la regla S-SENT-SEQ, con lo cual:
 . s1 s2 . 
00
Y 00 es tal que JqKBool00 = true.
Caso condicional:
p j= safeB(g)
p ^ g j= p1 fp1g s1 fq1g q1 j= q
p ^ :g j= p2 fp2g s2 fq2g q2 j= q
A-SENT-IF
fpg if g then s1 else s2 fi fqg
Sea  2 M una valuación tal que JpKBool = true.
Suponiendo las hipótesis de la regla, como p j= safeB(g), a partir del Teorema 3.1, se puede
garantizar que existe un x 2 ftrue; falseg : JgKBool = x.
Se divide la prueba en dos casos, según el valor de x:
1. Caso x = true.
En este primer caso Jp ^ gKBool = true, con lo cual también vale que Jp1K
Bool
 y por lo
tanto, a partir de la hipótesis inductiva, se sabe que:
 . s1 . 
0
Con 0 tal que Jq1KBool0 = true, por lo tanto JqK
Bool
0 .
92

 Caso m0  0.
Observar que si se usa q0 en lugar de p0, la regla para la semántica abstracta requiere
que q0 j= var > 0. Sin embargo esto no puede ser ya que m0  0.
Esta contradicción proviene del hecho de que inv ^ g j= q0 y sin embargo p j= inv,
con lo cual la guarda es necesariamente falsa.
Por lo tanto se aplica la regla de semántica operacional que finaliza la ejecución del
ciclo, de forma similar al caso x = false visto anteriormente.
 Tomar un m0 > 0 y suponer que vale la propiedad para cualquier valor menor a m0,
ver que la propiedad vale para m0.
Por razonamientos análogos a todos los hechos hasta aquí pero reemplazando p0 por
q0 y  por 0 localVars(s), se puede llegar hasta este punto.
Adicionalmente, como se sabe que el variante decrece, luego se tiene el variante m00
(el análogo a m0 en esta demostración) tal que m00 < m0. Por lo tanto se aplica la
hipótesis inductiva y se sabe que: 0 localVars(s) .while g :?! inv :# var do s od .
00
Falta ver que:
Jinv ^ :gKBool00 = true
 JinvKBool00 = true
Se puede ver por inducción en m0, el valor del variante en 0.
Si m0  0, luego 00 = 0. Ya se vió que JinvKBool0 = true.
Si m0 > 0 y se supone que la propiedad vale para valores más chicos que m0, ver que
vale para m0. En este caso se puede aplicar el mismo razonamiento pero con m0 en lugar
donde antes estaba m. Se llega a un m00 tal que m00 < m0, luego allí vale que el invariante
se preserva. Y una única aplicación de la regla para semántica operacional que continúa
la ejecución del ciclo garantiza que el invariante se preserva.
 J:gKBool00 = true
La única forma de finalizar la ejecución del ciclo es que g sea falso. Esto se puede demos-
trar por inducción en m0.
Si m0  0, ya se vió que como inv ^ g j= p0 j= var > 0, luego la única posibilidad es que
g sea falsa.
Si en cambio m0 > 0, se puede aplicar la hipótesis inductiva y el ciclo siempre termina
con la aplicación de la regla cuya hipótesis es que la guarda es falsa.
Caso llamado a un procedimiento:
pbcpi 7! pic j= P( proc)
9o1; : : : ; ok (pbcpi 7! oic ^ Q( proc)bpi 7! cpi; pi@pre 7! oic) j= q
A-SENT-CALL
fpg call proc(cp1; : : : ; cpk) fqg
Donde pars(proc) = p1; : : : ; pk
Suponer que se parte de una valuación  2 M tal que JpKBool = true.
Definiendo  como en la regla para semántica operacional para llamados a procedimientos, su-
cede que Jpbcpi 7! picKBool = true. Esto se debe a que sustituir los elementos en la fórmula es
equivalente a cambiarles su nombre en la valuación.
Por lo tanto, como pbcpi 7! pic j= P( proc) luego JP( proc)KBool = true.
95

Como  es seguro, se sabe que:
fP( proc)g body(proc) fQ( proc)g
Luego por hipótesis inductiva:
 . body(proc) . 0
Con 0 tal que JQ( proc)K
Bool
0 = true.
Con lo cual se cumplen las hipótesis de la regla SEM-SENT-CALL, por lo tanto:
 . proc(cp1; : : : ; cpk) . 
0
Con 0 definido en función de 0 tal como en la regla para semántica operacional de llamados a
procedimientos.
Falta ver que JqKBool0 , y como 9o1; : : : ; ok (pbcpi 7! oic ^ Q( proc)bpi 7! cpi; pi@pre 7! oic) j= q,
alcanza con ver que:
J9o1; : : : ; ok (pbcpi 7! oic ^ Q( proc)bpi 7! cpi; pi@pre 7! oic)K
Bool
0
Antes que nada observar la similitud con la regla de la asignación. Se está trabajando en este
caso sobre k variables a la vez, por lo tanto es necesario cuantificar existencialmente sus k valores
anteriores.
Tal como en el caso de la asignación, sigue valiendo p pero reemplazando los parámetros concretos
por sus viejos valores, denominados oi. Los valores que harán verdadera la fórmula son JcpiKInt ó
JcpiKArray , dependiendo del tipo de cpi.
Con tales valores se puede ver que pbcpi 7! oic es cierto, ya que JpKBool y justamente se están
reemplazando los parámetros concretos por su valor en .
La segunda parte se desprende del hecho de que JQ( proc)K
Bool
0 = true. A partir de la postcondi-
ción, se pueden reemplazar los parámetros formales por los concretos, del mismo modo que 0 se
construye a partir de 0, con lo cual la valuación no es afectada.
2
96

A.5. Demostración del Teorema 3.4
Sea s 2 Sentence;;0 y sea q 2 BoolExp0 . Si pre(s; q) = p luego fpg s fqg.
Dem:
Se demuestra por inducción estructural en s.
Caso asignaciones y creación de variables. Todos casos similares, observar por ejemplo la asignación
de enteros. Su cálculo de precondición establece que:
PRE-IASSIGN
pre(v i; q) = safeI(i) ^ qbv 7! ic
La semántica abstracta dice en ese caso:
p j= safeI(i) 9 v0 : Int (pbv 7! v0c ^ v = ibv 7! v0c) j= q
A-SENT-IASSIGN
fpg v i fqg
En este caso:
p = safeI(i) ^ qbv 7! ic
Puede verse fácilmente que:
safeI(i) ^ qbv 7! ic j= safeI(i)
Faltaría ver que:
9 v0 : Int ((safeI(i) ^ qbv 7! ic)bv 7! v0c ^ v = ibv 7! v0c) j= q
Lo cual es equivalente a:
9 v0 : Int (safeI(i)bv 7! v0c ^ (qbv 7! ic)bv 7! v0c ^ v = ibv 7! v0c) j= q
Observar que se reemplazan en q todas las apariciones de v por i, lo cual podría hacer que dicha
expresión resultante no fuerce q. Sin embargo también se conoce el hecho de que v = i. Se obvian
en este razonamiento las sustituciones de v por v0.
Caso sentencia vacía y secuenciamiento. Son triviales.
Caso condicional. La regla para el cálculo de precondiciones es:
pre(s1; q) = p1 pre(s2; q) = p2
PRE-IF
pre(if g then s1 else s2 fi; q) = safe
B(g) ^ (g ^ p1 _ :g ^ p2)
La semántica abstracta es determinada en este caso por:
p j= safeB(g)
p ^ g j= p1 fp1g s1 fq1g q1 j= q
p ^ :g j= p2 fp2g s2 fq2g q2 j= q
A-SENT-IF
fpg if g then s1 else s2 fi fqg
Se utiliza en este caso:
p = safeB(g) ^ (g ^ p1 _ :g ^ p2)
Por otra parte q es usado como q1 y también como q2. Por hipótesis inductiva se obtienen precon-
diciones p1 y p2 tales que satisfacen el teorema.
99

Caso ciclo. En este caso la precondición se calcula usando:
true j= safeB(inv) inv j= safeB(g) inv j= safeI(var)
inv ^ g j= p0 p0 j= var > 0
post(var0 var s; inv ^ g) = q
0
q0 j= inv q0 j= var < var0 inv ^ :g j= q
PRE-WHILE
pre(while g :?! inv :# var do s od; q) = inv
La semántica abstracta para este caso, obviando las condiciones para expresiones seguras, es
determinada por:
true j= safeB(inv) inv j= safeB(g) inv j= safeI(var)
p j= inv inv ^ g j= p0 p0 j= var > 0
fp0g var0 var s fq
0g
q0 j= inv q0 j= var < var0 inv ^ :g j= q
A-SENT-WHILE
fpg while g :?! inv :# var do s od fqg
Tal como en el caso del cálculo de postcondiciones se usa inv^g como p0. En este caso la respuesta
es p = inv, por lo tanto siempre se sabe que p j= inv.
Caso llamado a procedimiento. La precondición se calcula usando la siguiente regla:
1  i  k
PRE-CALL
pre(call proc(cp1; : : : ; cpk); q) = P( proc)bpi 7! cpic ^
(9a1; : : : ; ak(Q( proc)bpi 7! ai; pi@pre 7! cpic ) qbcpi 7! aic))
La semántica abstracta en este caso está dada por:
1  i  k pbcpi 7! pic j= P( proc)
9o1; : : : ; ok (pbcpi 7! oic ^ Q( proc)bpi 7! cpi; pi@pre 7! oic) j= q
A-SENT-CALL
fpg call proc(cp1; : : : ; cpk) fqg
En el caso del cálculo de precondiciones se cuantifica existencialmente los valores posteriores de
los parámetros concretos usando a1; : : : ; ak. De modo análogo la semántica operacional utiliza
o1; : : : ; ok para cuantificar los valores anteriores de los parámetros concretos.
Las sustituciones se hacen sobre lo que ya se sabía o sea, p en el caso de la semántica abstracta,
o sobre las anotaciones del procedimiento llamado en el caso del cálculo de precondiciones. En
ambos casos el resultado es equivalente.
2
100