Download UNIVERSIDAD SIM´ON BOLÍVAR Java + Especificaciones

UNIVERSIDAD SIMÓN BOLÍVAR
Ingenierı́a de la Computación
Java + Especificaciones
por
Gabriela Valentina Montoya Castillo
Proyecto de Grado
Presentado ante la Ilustre Universidad Simón Bolı́var
como Requisito Parcial para Optar al Tı́tulo de
Ingeniero en Computación
Sartenejas, Diciembre de 2005
UNIVERSIDAD SIMÓN BOLÍVAR
DECANATO DE ESTUDIOS PROFESIONALES
COORDINACIÓN DE INGENIERÍA DE COMPUTACIÓN
ACTA FINAL DE PROYECTO DE GRADO
Java + Especificaciones
Presentado por
Gabriela Valentina Montoya Castillo
Este proyecto de grado ha sido aprobado en nombre de la Universidad Simón Bolı́var por el
siguiente jurado examinador:
Prof. Blai Bonet
Jurado
Prof. Pedro Borges
Jurado
Prof. Ascánder Suárez
Profesor Guı́a
Prof. Jesús Ravelo
Tutor Académico
Sartenejas, Diciembre de 2005
Java + Especificaciones
por
Gabriela Valentina Montoya Castillo
Resumen
En este proyecto se plantea el diseño e implementación de una extensión a Java, para incluir las
herramientas necesarias para especificar clases mediante el establecimiento de contratos (del tipo
precondición, postcondición e invariante); esto busca ayudar a mejorar la elaboración del código
en Java, y facilitar la determinación de qué sección de código es la que esta fallando ante un caso
de prueba cualquiera. Se realiza una verificación dinámica de los contratos establecidos, esto es,
a momento de ejecución se verifica que el programa (con los parámetros actuales) cumpla con las
condiciones establecidas, lo cual, aunque no es demostración de que el programa siempre cumple el
contrato, contribuye a detectar instancias en las que el contrato es roto (esto es, contraejemplos).
Se siguieron los lineamientos de Java Modeling Language (JML), extensión de Java que permite
especificaciones y se encuentra en pleno desarrollo.
iii
Índice general
Resumen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1. Introducción . . . . . . . . . . . . . . . . . . .
1.1. Planteamiento y Formulación del Problema
1.2. Objetivos . . . . . . . . . . . . . . . . . . .
1.3. Justificación . . . . . . . . . . . . . . . . . .
1.4. Delimitación y Alcance . . . . . . . . . . . .
III
.
.
.
.
.
1
1
3
4
5
2. Marco Teórico . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.1. Antecedentes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.2. Bases Teóricas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
7
7
10
3. Marco Metodológico . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
12
4. Propuesta . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.1. Formalización de la Extensión . . . . . . . . . . . . . . .
4.2. Mecanismo para comprobar la validez de los programas
4.3. Análisis de Complicaciones . . . . . . . . . . . . . . . .
4.3.1. Herencia . . . . . . . . . . . . . . . . . . . . . . .
4.3.2. Apuntadores . . . . . . . . . . . . . . . . . . . .
4.3.3. Excepciones . . . . . . . . . . . . . . . . . . . . .
4.4. Ventajas sobre Extensiones ya Realizadas . . . . . . . .
4.5. Testing . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.5.1. Plan de Testing . . . . . . . . . . . . . . . . . . .
4.5.2. Usando JUnit para realizar las pruebas . . . . .
4.5.3. Usando TestJCR . . . . . . . . . . . . . . . . . .
.
.
.
.
.
.
.
.
.
.
.
.
14
14
17
17
17
18
18
19
19
20
21
21
5. Implementación . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
22
6. Conclusiones y Recomendaciones . . . . . . . . . . . . . . . . . . . . . . . . . . . .
25
Bibliografı́a . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
26
Glosario . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
iv
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
A. Código de los casos de prueba para JUnit . . . . . . . . . . . . . . . . . . . . . .
33
B. Formato de los casos de prueba de TestJCR . . . . . . . . . . . . . . . . . . . . . .
36
C. Programas en JML . . . . .
C.1. Programa tipo Algoritmos
C.2. Programa tipo Algoritmos
C.3. Programa tipo Algoritmos
.
.
.
.
37
37
37
39
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
42
1. Ejemplo de programa en JContractor . . . . . . . . . . . . . . . . . . . . . . . . .
45
2. Ejemplo de programa en JML . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
49
D. Detalles de Implementación
. . . . . . . . . . . . . . .
I: Factorial . . . . . . . .
I: Ordenamiento Burbuja
II: TAD Diccionario . . .
v
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
Capı́tulo 1
Introducción
1.1.
Planteamiento y Formulación del Problema
¿Qué son aserciones? En el ámbito de la programación imperativa son afirmaciones, predicados
que se deben cumplir en cierto punto de un programa. Sirven para verificar que se cumplan ciertas
condiciones que se dan por ciertas, que el programa deberı́a satisfacer en ese punto de la ejecución,
para comprobar que el programa está realizando lo que se cree que está procesando.
Las aserciones se pueden usar para verificar formalmente la correctitud de un programa, esto
mediante el uso de las mismas como precondiciones, postcondiciones, invariantes y aserciones
puntuales en el desarrollo del código. Se utilizan como base las teorı́as de Hoare [12] y Dijkstra
[8, 9] que definen la noción de correctitud de un programa imperativo, esto es: si se le da un estado
inicial que satisfaga la precondición indicada, cumplirá con obtener un estado final que satisfaga
la postcondición; ası́, realiza lo que se espera de él.
Java[15] es un lenguaje de programación muy popular en los últimos años, y cada vez son más
los grandes sistemas que son desarrollados usando Java como base. Se usa tanto en aplicaciones
de interés comercial, como cientı́fico o educativo; se usa en campos en los que puede llegar a ser
crı́tico su correcto funcionamiento. Esto es, una falla en el programa, un bug sin resolver, puede
llegar a ocasionar conflictos e incluso grandes pérdidas, tanto en materia económica como en otros
aspectos incluso más importantes (por ejemplo: salud, ambiente, etc.). Por tanto, se hace altamente
1
2
importante el desarrollo de programas en Java que se sepa que son correctos, que hacen lo que se
diseñó que deben realizar, y a este objetivo podemos acercarnos más utilizando aserciones en los
programas desarrollados en Java.
Aserciones en Java
Java[15] provee una instrucción:
assert <exprBooleana> o
assert <exprBooleana> : <valor>,
siendo <exprBooleana> la aserción a verificar en el punto donde se coloca esta instrucción y
<valor> un parámetro a pasar para dar un mensaje de error adecuado al manejador de excepciones, ya que en caso de que la aserción falle, esto es, sea falsa, se levanta una excepción.
Esta instrucción se utiliza para verificar que el programa que se está desarrollando se está
comportando en efecto como se ha estimado. Las limitaciones que presenta están estrechamente
relacionadas con el limitado conjunto de operadores que pueden tomar parte en las expresiones
booleanas a incluir (como <exprBooleana>). En ella sólo se pueden incluir las expresiones booleanas de Java, como lo son constantes (true y false), operadores unarios (!), operadores binarios
(&, ^, |, &&, ||), operadores ternarios (?:), relacionales (>, >=, <, <=, ==, !=) y funciones (cuyo
valor de retorno sea booleano). Estas expresiones, tal cual las ofrece Java, son inadecuadas para lograr el propósito de que mediante aserciones se analice la correctitud del programa, ya que
en muchos casos son insuficientes para especificar lo que deseamos expresar sobre el estado del
programa en un punto dado y en otros tienen un nivel de abstracción demasiado bajo, se pierde
la semántica de la especificación y se aumenta el grado de dificiltad para el programador. Hace
falta otros operadores lógicos adicionales, como lo es la implicación, para dar mayor claridad a las
aserciones (a pesar de que se podrı́a traducir a los operadores existentes), y cuantificadores (∀, ∃,
3
∑, ∏, ↑, ↓,
S
, ... ), además del manejo de las aserciones sobre clases (o tipos abstractos de datos)
y su uso adecuado en los métodos.
Todo esto se encuentra limitado por las facilidades que ofrece Java. Es por ello que proponemos
el desarrollo de una extensión la cual ofrezca expresiones adicionales a las de Java para lograr
especificar adecuadamente el código, y ası́ ayudar a garantizar la correctitud del programa, y
obtener códigos bien especificados, más confiables y fáciles de reutilizar adecuadamente.
1.2.
Objetivos
Objetivo General
Diseñar e implementar una extensión a Java que contemple las facilidades necesarias para la
inclusión de especificaciones.
Objetivos Especı́ficos
Definir el lenguaje extensión de Java.
Desarrollar el traductor de Java extendido a Java básico.
Analizar posibles complicaciones del Java extendido en relación con las teorı́as de correctitud
existentes.
Actividades Asociadas
Realizar revisión bibliográfica de diversas extensiones a Java
Estudiar las extensiones a Java previamente realizadas para inclusión de especificaciones;
evaluación de aspectos cubiertosy y pendientes en el desarrollo de las mismas.
4
Utilizar la herramienta Claire para la construcción de la gramática de Java; proponer mejoras
a la herramienta para vencer posibles limitaciones frente a otras existentes.
Profundizar en los conocimientos previos en especificación formal de programas.
Diseñar un plan de testing que, mediante la automatización, nos ayude a garantizar la
correctitud de los programas desarrollados a lo largo de este proyecto.
1.3.
Justificación
En un ambiente en el cual se pone tanto énfasis en la correctitud de los programas, como
lo es en el académico, es pertinente la creación de un lenguaje que ayude a los estudiantes, en
primer pero no único lugar, a realizar sus programas de manera más confiable, contando con una
verificación a tiempo de ejecución de los contratos que plantean como válidos para su código. Y
en general, un lenguaje con tales caracterı́sticas incrementa la confianza que se tiene en el código
producido haciendo uso de especificaciones, y permite comprobar que el programa cumple con las
condiciones establecidas en instancias especı́ficas. Como se mencionó con antelación, se sabe el
tremendo auge que está teniendo Java; por tanto también se considera importante que desde el
inicio los estudiantes se adentren en el uso y producción de código Java. Luego, resulta importante
el planteamiento de extender Java para incluirle especificaciones, y que estas especificaciones usen
en la medida de lo posible el mismo estilo de sintaxis de Java para, en primer lugar, facilitar el
aprendizaje simultáneo de Java y la extensión planteada, ası́ como, en el caso más general, facilitar
al usuario el aprendizaje de este lenguaje de especificación.
Por otra parte, en el ámbito industrial, también se están realizando verificaciones formales de
código Java con especificaciones. Un caso particular de esto es VerifiCard[14], que es un proyecto
cuyo objetivo es garantizar que las nuevas Smart Cards que sean más seguras; para esto hacen
5
uso de la especificación formal, y de la herramienta LOOP[26] (la cual utiliza un demostrador de
teoremas para verificar las obligaciones de prueba derivadas de la especificación).
1.4.
Delimitación y Alcance
La extensión planteada se limita a la versión 1.5 de Java, que es la más reciente. Para este
proyecto de grado se plantea al menos realizar la estructuración y análisis de los aspectos a
contemplar en la extensión completa a Java, mas por razones de tiempo, se realizará sólo una
primera versión del traductor, la cual en manera general reconozca código Java extendido, elabore
los árboles abstractos del mismo y genere código Java básico. Los aspectos que queden pendientes
se dejarán documentados en este trabajo para su estudio posterior.
Siendo este proyecto realizado en Venezuela y siendo Java el nombre de una semilla de café,
se decidió que el nombre de este proyecto debı́a indicar algo propio de este paı́s y siendo una de
las bebidas tı́picas el carajillo, que consiste en café con ron u otro licor, se escogió Carajillo o
JCR, abreviación de Java Con Ron, como nombre para el proyecto completo planteado. En las
secciones subsiguientes se referirá al proyecto completo como JCR, y a este proyecto de grado
como este proyecto. En el capı́tulo 2, se presenta una revisión de los antecedentes de este tipo de
extensión a Java, ası́ como también una revisión de las bases teóricas que sustentan el desarrollo
de JCR y dan sentido al mismo. Luego, en el siguiente capı́tulo (3) se explica la metodologı́a
seguida en el desarrollo del proyecto. Luego, en el capı́tulo 4 presenta formalmente la extensión
planteada, se realiza un análisis de las complicaciones del lenguaje a tener presentes en el diseño
e implementación de la extensión, y se estudia la misma comparativamente frente a otras ya
existentes. También se plantea el plan de testing a seguir para evaluar el funcionamiento de la
extensión y su traductor. Luego, en el capı́tulo 6 se presentan las conclusiones a las que se llegó
gracias a la realización de las actividades concernientes a este proyecto y también se presentan
6
una serie de recomendaciones al momento de realizar trabajos similares y los posibles puntos de
continuidad de este proyecto en el ámbito de JCR. Se incluye un glosario para aclarar algunos
términos utilizados a lo largo de este informe y algunos apéndices entre ellos destaca el apéndice D,
donde se incluyen una serie de acotaciones acerca del desarrollo de este proyecto, donde se pondrán
de manifiesto las soluciones que se le dieron a algunos conflictos presentados en el desarrollo debido
al alcance del analizador sintáctico utilizado.
Capı́tulo 2
Marco Teórico
2.1.
Antecedentes
Una primera referencia, a pesar de no ser una extensión a Java, es sin duda a alguna Eiffel[20],
lenguaje de programación que desde su creación incluye especificaciones y, por tanto, permite
establecer contratos entre las clases. Se establecen precondiciones, postcondiciones e invariantes
de clases (con las palabras reservadas: require, ensure e invariant respectivamente).
Con respecto a extensiones a Java para mejorar su carencia de facilidades para establecer
especificaciones, existe jContractor[16], propuesto en 1999 por Murat Karaorman, Urs Hölzle y
John Bruno en el artı́culo “jContractor: a Reflective Java Library to Support Design by Contract”
y desarrollado por Parker Abercrombie, el cual es una herramienta que permite la inserción de
precondiciones, postcondiciones e invariantes de clases, directamente en el código escrito en Java,
mediante el uso de métodos que siguen un patrón preestablecido en el nombre, contenido, parámetros y valor de retorno. Estos métodos se pueden incluir tanto en la clase misma en la que se
desarrolla el programa o ser incluidos en una clase adicional, lo cual es muy útil si no se tiene
el código fuente de la clase a la que se le desea colocar las aserciones (esto es, si sólo se tienen
los “.class” ) o si se desea estructurar estos métodos en una clase adicional para darle mayor
claridad al código. Esta herramienta usa una librerı́a para ampliar el conjunto de operadores booleanos que se pueden utilizar en los contratos, Java Quantification Library (JaQuaL)[1], la cual
7
8
incluye una clase Logical y como métodos los operadores adicionales, como lo son la implicación
(Logical.implies(<ExprBooleana>, <ExprBooleana>)), y abstracciones de los cuantificadores
sobre colecciones (ForAll.in(<Collection>).ensure(<ExprBooleana>)). Esta extensión requiere, al momento de ejecutar el programa, que la lı́nea de comando sea de la siguiente manera:
java jContractor <nombrePrograma>, si los métodos que definen el contrato están en la
misma clase, o,
java jInstrument ./ <nombrePrograma>.class
java <nombrePrograma>, en caso de que estos métodos se definan en una clase independiente.
JContractor actualmente se encuentra en fase alfa, por lo cual no es fácil conseguir documentación.
Se puede observar un ejemplo de un programa especificado con JContractor en el anexo 1.
Otra extensión de Java con aserciones es Java Modeling Language (JML)[17]. Explican su
utilización como lenguaje para diseño por contratos Gary T. Leavens y Yoonsik Cheon en el artı́culo
“Design by Contract with JML”. En esta extensión las aserciones se especifican en la documentación
(en la cual todas las lı́neas que son aserciones inician con @): con requires para la precondición;
ensures para la postcondición; signals para postcondiciones excepcionales, o cuando se lanza una
excepción durante la ejecución; y public invariant para especificar un invariante de clase cuando
los objetos son visibles al usuario, especı́ficamente al final del constructor e inicio y fin de cada
uno de los métodos de la clase. Además, en las aserciones se pueden incluir operadores booleanos
adicionales a los provistos por Java como lo son implicaciones (==>), consecuencia (<==), doble
implicación (<==>), inequivalencia (<=!=>), variables de especificación (\old(<Variable>) para
indicar el valor que tenı́a al inicio de un bloque/método una variable) y cuantificadores (\forall,
\exists, \sum, \product, \min, \max, \num_of). Esta extensión requiere un compilador adicional
(“JML compiler”, que se usa con el comando jmlc) o se puede usar con una herramienta de testing,
9
como lo es “unit” (en este caso jmlunit). Su documentación aún se encuentra en desarrollo. Se
puede apreciar un ejemplo de un programa especificado con JML en el anexo 2.
Esta última, por su trayectoria (ha estado en desarrollo desde 1998 hasta el presente), porque
varias de las otras extensiones se han ido apegando a su notación, y por la cantidad de herramientas
que se han ido ajustando para prestar soporte a este lenguaje, se ha considerado un modelo a seguir
para el desarrollo de este proyecto, ya que establece lineamientos de cómo adaptar los aspectos de
diseño por contratos de Eiffel a Java, siguiendo las caracterı́sticas y notación propias de Java, para
ası́ facilitarle a los usuarios el aprendizaje del lenguaje extendido que permite especificaciones.
Entre las extensiones que usan las especificaciones de JML están las siguientes: Korat[5] (que
permite el testing automático incluyendo la generación de casos de prueba), LOOP[26] (que genera
las obligaciones de prueba y provee acoplamiento con un probador de teoremas), ESC/Java[7] (que
detecta errores a tiempo de compilación).
Referente al tema del manejo de la herencia entre clases, se tiene la alternativa planteada en
el artı́culo “Contract Soundness for Object-Oriented Languages”[10] de Robert Bruce Findler y
Matthias Felleisen, en donde se presenta una propuesta, al menos teórica, frente a la debilidad
que tienen las extensiones existentes en este ámbito. Y es que aunque en el desarrollo teórico de
las extensiones se evidencia que los diseñadores tienen presente que se debe preservar la herencia
de las especificaciones agregadas, tal y como lo expresan Leavens y Cheon en [17], es importante
garantizar que los subtipos sean behavioral subtypes, y puedan manejar los casos que manejaba la
superclase, lo cual se resume en que sean teoremas las siguientes implicaciones:
presuperClase ⇒ presubClase y postsubClase ⇒ postsuperClase
pero hasta ahora lo que verifican es:
presuperClase || presubClase y postsubClase && postsuperClase
(♦)
10
Lo cual no garantiza ninguna relación entre la subclase y la superclase. Entonces se permiten
subtipos que en realidad pueden no cumplir los contratos de la superclase, y sólo lanzan excepción
si se violan ambas precondiciones o alguna de las postcondiciones. También se obliga a las subclases
a ejecutarse en momentos en los que el estado del programa no garantiza su propia precondición,
ya que en estos casos cumplir la de la superclase no conlleva a cumplir la propia.
2.2.
Bases Teóricas
El planteamiento de este proyecto se sostiene en una serie de teorı́as que justifican el uso de la
especificación de programas y dan confianza en la subsecuente correctitud garantizada. La primera
de estas teorı́as es la propuesta por Hoare[12], que establece la noción inicial de razonamiento
deductivo sobre programas, estableciendo mediante axiomas (similarmente como se hace en la
matemática tradicional) las propiedades y condiciones que debe cumplir el programa al realizar
las acciones básicas del lenguaje (como por ejemplo asignación de valores a variables) y su posible
uso para probar la correctitud de un programa completo mediante el uso de la especificación,
que no es más que el establecimiento formal y claro de las propiedades que el programa cumple
en ciertos puntos (o estados), como el estado inicial y final (precondición y postcondición). Esta
teorı́a propone que si un programa cumple con una aserción en el estado inicial (precondición) y
el programa termina, entonces termina en un estado que cumple cierta propiedad (postcondición),
luego es una teorı́a de correctitud parcial, también llamada correctitud condicional. Aunque quien
realiza esta formalización ciertamente es Hoare, quien primero abordó el tema y realizó las primeras
observaciones fue Floyd[11]. Luego Edsger W. Dijkstra[8, 9] propone teorı́as que amplian esta
noción de correctitud, introduciendo la noción del transformador de predicados wp, que no es más
que la más débil precondición que se debe cumplir para que una instrucción genere estados que
satisfacen una postcondición en particular, y con esta noción obliga a las instrucciones a terminar
11
y a terminar de manera adecuada (acorde con la postcondición).
Otra teorı́a que se siguió es la de Liskov y Wing, expuesta en el artı́culo “Behavioral Subtyping Using Invariants and Constraints”[19], donde proponen las condiciones que debe cumplir un
subtipo, para estar bien definido, y estas condiciones son las de sustitución. A tiempo de ejecución
un supertipo debe poder ser sustituido por cualquiera de sus subtipos sin generar conflictos con
las especificaciones, esto ya que ambas deben estar relativamente bien definidas. Respecto a la
relación evidente entre ambas clases, debe cumplirse que la precondición de la subclase puede ser
más débil que la de la superclase y que la postcondición de la subclase puede ser más fuerte que
la de la superclase. Y esto corresponde con otra teorı́a (importante en materia de especificación
formal de programas): teorı́a de refinamiento de Morgan[21] sobre instrucciones de especificación,
ignorando algunos detalles, esto es:
[ pre, post] v [ pre0 , post0 ], si [ pre ⇒ pre0 ] y [ post0 ⇒ post]
que expresa que una instrucción de especificación es refinada por otra, si para cualquier estado
del programa la precondición de la refinada implica la precondición del refinamiento y la postcondición del refinamiento implica la postcondición de la refinada; siendo estos refinamientos los
establecidos por cada método que la subclase sobreescribe de su superclase y estas implicaciones
las mencionadas por Liskov y Wing[19].
Capı́tulo 3
Marco Metodológico
En este capı́tulo se describe la metodologı́a seguida en el desarrollo de este proyecto.
Se siguió la metodologı́a Crystal Clear[6], por el tamaño del proyecto y del equipo de trabajo.
Esta metodologı́a de la familia de metodologı́as Crystal es la indicada para equipos de trabajo
pequeños, en el caso de este proyecto: una persona.
Debido a las condiciones de trabajo se prescindió entonces de la serie de entregables tı́picos del
desarrollo de software con un nivel mayor de complejidad de las condiciones (equipo de trabajo
de mayor tamaño y proyecto de mayor duración y extensión), y se sustituyeron por entrevistas
regulares con el cliente (tutor del proyecto de grado), en las cuales se informaba del estatus del
proyecto y se fijaban conjuntamente las próximas prioridades en las cuales hacer énfasis. Además,
tal y como lo recomienda esta metodologı́a, se le dió importancia desde el inicio del desarrollo a la
fase de testing del proyecto, a plantear las maneras en que se probarı́a cada uno de los programas
generados en el proceso de desarrollo. Y, además del testing realizado continuamente, se trabajó
en un plan sistemático y automatizado que facilitara ese proceso, a efectos de garantizar que se
realizarı́an todas las pruebas que se consideraran necesarias. Aunque una caracterı́stica de esta
metodologı́a es su flexibilidad respecto a la forma de trabajo del programador, se puede resumir
en: entrevistas con el cliente, desarrollo y pruebas; esto de manera iterativa.
Este proyecto fue desarrollado de manera incremental, se comenzó con la elaboración de un
12
13
pequeño reconocedor de expresiones booleanas básicas y paulatinamente se fueron considerando
los demás elementos de Java.
Capı́tulo 4
Propuesta
Se plantea la elaboración de una extensión de Java que intente cubrir el concepto de diseño por
contrato completamente, intentando que no queden ambigüedades referentes a ningún aspecto de
cómo se deben manejar las precondiciones y postcondiciones, tanto en la relación clase-superclase
como en las llamadas a métodos. Para ello también se plantea la definición y elaboración de
las expresiones extendidas, al agregar implicación y cuantificadores a las expresiones de Java. Se
plantea el usar como referencias para el diseño las citadas entre los antecedentes (especialmente
JML) y, para la implementación, estudiar la posibilidad de adaptar a las necesidades de esta
extensión el código de GaCeLa[24] (implementación de GCL[8] desarrollada en la Universidad
Simón Bolı́var por Ascánder Suárez). Se sigue la sintaxis y semántica del lenguaje JML ya que,
como se expuso en los antecedentes, esta propuesta es muy aceptada en la actualidad y cumplen
con los requerimientos planteados al inicio de este proyecto. Ejemplos de especificación con JML,
de programas tipo Algoritmos I y Algoritmos II, son presentados en el apéndice C.
4.1.
Formalización de la Extensión
La extensión será un superconjunto de Java. Para diferenciar lo que pertenece a Java originalmente y lo que se ha incluido, y no causar problemas al compilar el código en Java, todo lo
14
15
perteneciente a la extensión debe usarse dentro de las anotaciones-JML, que no son más que comentarios válidos en Java que inician con un sı́mbolo ’@’. Se debe incluir un conjunto más amplio
de expresiones, que permita enriquecer la expresividad de este lenguaje, para ası́ en un más alto
nivel lograr especificaciones más concisas y precisas. Los operadores a incluir son las siguientes:
implicación, denotado por ==>.
consecuencia, denotado por <==.
equivalencia, denotado por <==>.
inequivalencia, denotado por <=! =>.
cuantificaciones universal, existencial, sumatoria, productoria, minimoria, maximoria y cantidad de elementos, denotados respectivamente por \forall, \exists, \sum, \product,
\min, \max, \num_of.
subtipo, denotado por <:.
Además, se incluyen cláusulas y modificadores diversos propios de JML que ayudan a especificar
mejor el comportamiento de las clases. Entre ellos caben destacar:
model, es un modificador que indica que la clase o campo al que se le atribuye es solamente
visible para las especificaciones; esto es, su uso fuera de las anotaciones-JML no tiene sentido.
spec_public y spec_protected, son modificadores que cambian el nivel de privacidad de
la especificación, es decir la hace visible a más niveles a pesar del modificador que pueda
contener la clase o campo.
pure, indica que un método no tiene efectos de borde y esto se hace para permitir el uso
de estos métodos en las especificaciones. En JML no se verifica que un método declarado
16
con este modificador esté, realmente, libre de efectos de borde; tal verificación requiere de
un análisis no trivial de todas las instrucciones y expresiones usadas en incluso los métodos
que se invoquen en el mismo
requires, ensures y signals, para indicar la precondición, postcondición y postcondición
excepcional (en caso de que ocurra alguna excepción), respectivamente.
invariant, palabra clave que indica que el predicado a continuación de ella es el invariante
de clase.
loop_invariant, palabra clave que indica que el predicado a continuación es el invariante
de ciclo.
weakly, modificador que indica que una clase no tendrá behavioral subtypes, si no weak
behavioral subtypes, ya que las subclases no heredan los history constraints, que indican la
relación que debe existir entre un estado del programa y los posibles siguientes estados del
mismo.
refine, palabra clave que se usa en la clausula de refinamiento, bien sea para indicar que
la clase es refinada por otra o que es un refinamiento de otra (distinguiendo esto según la
terminación del archivo)
Entre otras particularidades que permite la detallada especificación del código en JML (que son
descritas en más detalle en el manual de referencia de JML[18]), cabe mencionar que se permite
declarar e interactuar con conjuntos por comprensión.
17
4.2.
Mecanismo para comprobar la validez de los programas
Existen diversas maneras de hacer uso de las especificaciones para comprobar que un programa
está cumpliendo con el contrato establecido. Una de ellas es la verificación formal de correctitud
de teoremas, esto es, se verifica que los predicados correspondientes a las especificaciones son
válidos en toda instancia; realizar esto de manera automatizada no es algo sencillo aunque en
la actualidad existen verificadores de teoremas, no son capaces aún de lograr realizar todas las
pruebas necesarias. Otra manera de utilizar estos contratos es mediante una verificación dinámica,
que es en el momento de ejecución del programa: con los parámetros actuales se chequea que se
cumplan las condiciones. Esta forma tiene ciertas limitaciones, y es que no se comprueba realmente
que el programa es válido para toda instancia, se chequea que es válido para una instancia de
ejecución. Sin embargo, sólo esto, ayudado por un buen plan de testing que cubra muchas de
las posibles situaciones a las que se puede enfrentar el programa, ayudan a tener confianza en el
código que se produce.
4.3.
4.3.1.
Análisis de Complicaciones
Herencia
El manejo adecuado de la herencia es una complicación, ya que la manera de realmente garantizar que se cumplen las condiciones adecuadas entre clase y superclase, requieren prueba de
teoremas para demostrar que las condiciones de refinamiento que surgen de las especificaciones
son válidas. Estas condiciones a demostrar serı́an las implicaciones correspondientes a behavioral
subtypes indicadas en (♦), en la sección 2.1 (en la página 7), y que son las exigidas por Liskov y
Wing en [19], como se indica en la sección 2.2 (en la página 10).
18
Se plantea realizar sólo la verificación dinámica de que se cumplen ambas condiciones: las correspondientes a la superclase y a la subclase (esto en precondiciones, postcondiciones e invariantes
de clase). Chequeando esto estarı́amos limitando las posibilidades de las subclases, pues aceptarı́an
contratos que su superclase hubiese aceptado, pero no se permite la posibilidad de que exista una
situación en la que una subclase se use en un momento en el que por ejemplo, su precondición no
se cumple pero sı́ la de su superclase.
4.3.2.
Apuntadores
En un lenguaje como Java, en el cual los arreglos y las clases se manejan mediante apuntadores,
por lo cual es posible tener aliasing, se hace necesario al momento de revisar la correctitud de un
código considerar las complicaciones determinadas por esto. Para que las especificaciones expresen
exactamente lo que proponemos y no quede lugar a posibles conflictos (generados por tener, al
menos, dos apuntadores a un mismo objeto) parece adecuado seguir el mismo razonamiento de
John Reynolds en su artı́culo “Separation Logic: A Logic for Shared Mutable Data Structures”[22],
y establecer que en lo relativo a objetos pasados por referencia hay manera, en las aserciones, de
indicar que los objetos se ubican en distintas partes de la memoria. De momento, no se cuenta
con un diseño ni una implementación formal de esto para Java/JML. En etapas futuras de JCR,
se plantea hacer énfasis en el desarrollo de ésto.
4.3.3.
Excepciones
Los programas en Java tienen la posibilidad de tener y especificar diversas condiciones de
terminación excepcional, debido a las condiciones de ejecución y a que hay factores que el programador no puede controlar (tales como que el usuario introduzca datos que generen problemas,
como lo puede ser 0 como denominador de una división), y aunque todas estas salidas producen
excepciones, y en Java todas son subclases de la clase Exception, es adecuado poder indicar, para
19
cada una, qué condición cumplen las variables del programa en caso de que se produzca alguna
de ellas, al momento de especificar el código y establecer el contrato de la clase. En [13] se puede
consultar una formalización de cómo se trata este aspecto en Java. Esto se especifica mediante
la cláusula signals en JML, y por tanto en JCR, donde se establece ante cierta excepción qué
condición cumplen las variables del programa.
4.4.
Ventajas sobre Extensiones ya Realizadas
Se quiere mejorar el tratamiento que se le está dando a la verificación de subtipos. Esto es, se
quiere chequear a tiempo de ejecución que los subtipos que se declaren sean behavioral subtypes
según la definición dada por Liskov y Wing[19]. Sólo en términos de verificación dinámica de JCR
sin un demostrador de teoremas, se ha propuesto verificar la conjunción de las condiciones (bien
sea precondiciones, postcondiciones o invariantes de clase). Se desea asegurar el cumplimiento de
las implicaciones adecuadas y con este mecanismo tenemos una buena aproximación, a nivel de
verificación dinámica, a lo que se desea. Esta es una significativa mejora en relación a JContractor
y JML (ver información al respecto en “Antecedentes”, sección 2.1 página 7).
Además, se plantea la posibilidad de realizar modificaciones a JCR, a mediano plazo, para
incluirle algunas ventajas adicionales, como puede ser incluir tipos algebraico-libres como los que
tiene Haskell[4] (que es un proyecto en GaCeLa[24]), lo cual, se sabe, está fuera del contexto de
Java como fue definido originalmente, pero podrı́a realizarse un análisis de la conveniencia de esta
posible modificación.
4.5.
Testing
El proceso de testing es una fase fundamental en el desarrollo de software. En esta fase se
verifica que el software cumpla con los requerimientos del proyecto, entre estos los niveles de
20
calidad adecuados relativos principalmente a que esté libre de errores. Esta parte del desarrollo
es muy importante y compleja, ya que al ser completada se puede lanzar y distribuir el producto.
Hay que tener una idea clara de cómo se va a realizar el testing, entre otras cosas qué aspectos se
desean probar, y qué tan exhaustivas serán las pruebas a realizar, hallando la relación adecuada
entre costo del testing y calidad del producto.
Se plantea llevar una fase de testing iterativa acorde al desarrollo iterativo incremental que
tenga el proyecto, el cual inicia por un reconocedor y evaluador que reconozca las expresiones booleanas básicas incluidas en Java, irle incorporando las extensiones tanto de expresiones booleanas
sencillas, como la implicación, como los cuantificadores, expresiones comparativas y aritméticas,
y ası́ hasta que el software esté completo, incluyendo instrucciones, clases, modelos, etcétera, de
manera que sea capaz de trabajar con programas completos.
4.5.1.
Plan de Testing
Como referencias para la elaboración de este plan se tomaron los lineamientos de Rational,
en especı́fico de su metodologı́a Rational Unified Process (RUP)[23, 25], en donde se expone la
problemática inherente a la elaboración de los planes de testing. Siguiendo estos lineamientos,
se plantea la elaboración de un plan de testing para cada una de las versiones a completar en
el transcurso de la elaboración de este proyecto. Cada plan consta de una especificación de los
aspectos a evaluar del software (qué queremos probar en cada caso), y el conjunto de casos de
prueba especı́ficos. Además, el proceso de testing se desea automatizar, mediante una herramienta
de testing que se plantea realizar, ya que aunque el proceso de testing fue realizado con JUnit[3]
en tempranas etapas del proyecto, con su uso se pierde parte del testing planteado para este
proyecto, como lo es el reconocimiento sintáctico. Luego, gracias a la automatización, la ejecución
y verificación de los resultados será más rápida y las pruebas pueden ser acumulativas, esto es,
21
que luego de cada iteración en la cual se solventen algunas fallas, se pueda con facilidad retomar
todos los casos con los cuales el programa funcionaba bien y comprobar que sigue trabajando bien,
además de verificar si los casos en los que fallaba se ha solucionado dicha falla; también se puede
incluir nuevos casos de prueba que se crean convenientes y necesarios.
4.5.2.
Usando JUnit para realizar las pruebas
JUnit es un software que facilita el proceso de testing del software en desarrollo. Está diseñado
para que su uso en repetidas ocasiones sea sencillo. Una vez que se han creados los casos de prueba,
basta con solicitar que se vuelvan a evaluar, incluso luego de que se le han hecho modificaciones
al código de las clases que se están desarrollando, sin tener que reescribir los casos de prueba, en
la mayorı́a de los casos (a menos claro, que se modifiquen la estructura o nombres de las clases
involucradas en la prueba).
Las pruebas, para hacer uso de esta herramienta, deben estructurarse en clases, subtipo de
TestCase, y en ellas definirse como métodos, tal y como se ilustra en el apéndice A, donde se
encuentra el código correspondiente a algunos de los casos planteados.
4.5.3.
Usando TestJCR
JCR contiene varios puntos de inicio para la gramática, lo cual facilita el testing de cada una
de las subpartes del reconocedor de la misma y, por supuesto, su uso en diversos contextos, ya que
se puede contar sólo con un reconocedor de expresiones, o con un reconocedor de instrucciones
(aunque ya incluirı́an expresiones), o un reconocedor de clases completas. Se tiene en un archivo el
conjunto de casos de prueba con sus respectivas respuestas en un formato adecuado (ver apéndice
B), y por salida estándar nos indica para cada caso si los resultados fueron los esperados y el
porcentaje y la cantidad de casos acertados y fallados.
Capı́tulo 5
Implementación
La verificación dinámica planteada en la sección 4.2 del capı́tulo 4 se realizó en este proyecto
mediante la traducción del código JCR (Java extendido) a Java básico. Luego la verificación
dinámica, una vez realizada la traducción, recae sobre el compilador original de Java.
A medida que se realiza el reconocimiento del código de JCR se van construyendo los árboles
abstractos correspondientes a las expresiones e instrucciones. La estructura del árbol resultante
luego es traducida a Java, y éste es el código que luego es ejecutado y que por tanto verifica, para
la instancia particular, que se cumplan las especificaciones formales incluidas en las anotaciones
tipo JML que se encontraban en el código original correspondiente.
Para la realización de este proyecto se contó con la librerı́a de árboles abstractos del lenguaje
GaCeLa[24]. GaCeLa, como se mencionó en el capı́tulo 4, es una implementación del lenguaje
GCL[8], y su compilador al reconocer este lenguaje como entrada, construye los árboles abstractos
de sus estructuras (expresiones, instrucciones y funciones entre otros) correspondientes; para su
ejecución se traducen estos árboles a código Java y luego es el código Java el que se compila y
ejecuta al momento de querer ejecutar el programa que originalmente estaba en GaCeLa. Esta
librerı́a sirvió de punto de partida y muchas de sus estructuras son reutilizadas ı́ntegramente; sin
embargo algunas de ellas fue necesario adaptarlas a las necesidades de JCR, puesto que en GaCeLa
no se contemplan las mismas instrucciones y expresiones. Por esto se tuvieron que incluir algunos
22
23
tipos de árboles nuevos y modificar algunos de los existentes para que contemplaran las nuevas
estructuras.
Se utilizó la herramienta Claire para elaborar el reconocedor de Java extendido, tal como se
propuso en el capı́tulo 1. El esquema de reconocimiento LALR(1) de dicha herramienta limitó el
reconocimiento del lenguaje; las modificaciones que se tuvieron que hacer al lenguaje originalmente
diseñado se presentan en el apéndice D.
Como referencia principal, se tomaron The Java Language Specification[15] y el manual de
referencia de JML[18]; esto para seguir JML como modelo de extensión, pero adaptado a la versión
1.5 de Java (JML actualmente está disponible para Java 1.4). Además se tomó como referencia
inicial el reconocedor de C. Scott Ananian de Java 1.5, construido con la herramienta JavaCup[2];
algunas maneras particulares de solucionar conflictos respecto al reconocimiento fueron adaptadas
del mismo. Las últimas modificaciones a esta versión son de julio de 2003; por esto y quizás
por algunos conflictos en JavaCup, hay elementos de Java 1.5 que no están presentes en ese
reconocedor, como lo son las anotaciones de Java.
En el desarrollo de JCR se llegó hasta reconocer todo el lenguaje extendido contemplado
en el diseño (ver ’Propuesta’, capı́tulo 4), con las limitaciones especificadas en el apéndice D,
pero sólo se llegó a construir los árboles (y por tanto generar el código Java correspondiente)
de las expresiones e instrucciones convencionales (entendiendo por esto que se dejaron de lado
las instrucciones que incluyen declaración de clases, instrucciones sincronizadas, etiquetadas, de
manejo de excepciones try-catch/throws, enumeraciones y las complicaciones intrı́nsecas a las
llamadas de métodos). En relación con las cláusulas de JML, se reconocen todas mas sólo se
incluyen en la traducción a árboles (y por tanto a código Java) las más básicas, entre las cuales se
consideraron las correspondientes a especificación de precondición, postcondición, invariantes (de
ciclo y clase) y cota (de ciclo).
24
Respecto al testing, se realizaron pruebas con códigos de diversos tamaños (menos de 500 lı́neas,
entre 1000 y 2000 y más de 2000 lı́neas), mas por razones de tiempo no se concretó el desarrollo de
TestJCR y por tanto tampoco la automatización del proceso, lo cual queda pendiente para futuras
etapas del desarrollo de JCR.
Capı́tulo 6
Conclusiones y Recomendaciones
A lo largo del desarrollo de este proyecto se pudo evidenciar la cantidad de implementaciones,
de lenguajes (en particular Java) con especificaciones, que han habı́do en los últimos años, aunque
por razones de simplicidad, se mostraron sólo las que se consideraron pertinentes bien por su gran
desarrollo o uso, por su particular enfoque o por su importancia referencial.
La gramática de Java es bastante extensa y nada sencilla de convertir en un reconocedor. En
relación a esto, aunque se logró estructurar toda la gramática de Java-extendido con la herramienta Claire, se evidenciaron limitaciones en el reconocimiento debido al algoritmo LALR(1),
utilizado por la herramienta, y por tanto se tuvieron que hacer algunas concesiones, las cuales,
lamentablemente, alteran el lenguaje en reconocimiento (ver apéndice D).
Se debe tener especial cuidado al tomar temas que están en pleno desarrollo, como JML, ya
que su documentación es limitada y en constante cambio. Ası́ mismo, se debe estar muy seguro de
cómo se implementan los modelos teóricos, ya que a pesar de tener conocimiento de las condiciones
de refinamiento que se deben cumplir en las clases y subclases, se pasó por alto su manejo adecuado
en la implementación de JML[17] y jContractor[16] respectivamente.
Con el desarrollo de este proyecto de grado se ha profundizado y puesto en práctica una
serie de conocimientos adquiridos a lo largo de la carrera, ası́ como la ejercitación del proceso de
investigación.
25
26
Recomendaciones
Se recomienda realizar una modificación a la herramienta Claire para permitir, aunque sea
a nivel lexicográfico, tener acceso al contexto derecho de los sı́mbolos para ası́ lograr un mejor
reconocimiento.
Ası́ mismo, para darle continuidad a JCR se recomienda mejorar este reconocedor solucionando los detalles de implementación documentados en el apéndice D, y ası́ mismo tomar en
consideración las complicaciones aquı́ analizadas y otras posibles que se escaparon del presente
estudio, y plantear posibles soluciones. También puede ser interesante llevar a cabo una fase de
testing más amplia, y utilizar JCR para programas de mayor tamaño.
Bibliografı́a
[1] Parker Abercrombie. Libreria JaQuaL, 2002.
URL http://jcontractor.sourceforge.net/doc/jaqual/api/index.html
[2] C. Scott Ananian. Gramática CUP de Java versión 1.5, Julio 2003.
URL http://www.cs.princeton.edu/~appel/modern/java/CUP/javagrm.tar.gz
[3] Kent Beck y Erich Gammma. JUnit Cookbook.
URL http://junit.sourceforge.net/doc/cookbook/cookbook.htm
[4] Richard Bird. Introduction to Functional Programming using Haskell. Prentice Hall, segunda
edición, 1998.
[5] C. Boyapati, S. Khurshid y D. Marinov. Korat: Automated testing based on Java predicates. En Proceedings of the 2002 International Symposium on Software Testing and Analysis
(ISSTA), Rome, Italy, July 22–24, 2002. 2002.
URL http://citeseer.ist.psu.edu/boyapati02korat.html
[6] Alistair Cockburn. Crystal Clear : A Human-Powered Methodology for Small Teams. Addison
Wesley Professional, 2004.
[7] Compaq Research Center. Extended static checker ESC/Java.
URL http://www.research.digital.com/SRC/esc/Esc.html
27
28
[8] Edsger Wybe Dijkstra. Guarded commands, nondeterminancy and formal derivation of programs. Communications of the ACM, 18(8):453–457, Agosto 1975. ISSN 0001-0782.
[9] Edsger Wybe Dijkstra. A Discipline of Programming. Prentice-Hall series in Automatic
Computation, Englewood Cliffs, N.J., 1976.
[10] Robert Bruce Findler y Matthias Felleisen. Contract soundness for object-oriented languages.
En ACM Conference on Object Oriented Programming, Systems, Languages and Applications
(OOPSLA’01), páginas 1–15. 2001.
URL http://www.ccs.neu.edu/scheme/pubs/oopsla01-ff.pdf
[11] Robert Floyd. Assigning meanings to programs. En J. T. Schwartz, editor, Mathematical
Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics 19, páginas
19–32. American Mathematical Society, Providence, 1967.
[12] Charles Antony Richard Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–583, Octubre 1969.
[13] Bart Jacobs. A formalisation of java’s exception mechanism. Informe Técnico CSI-R0015,
University of Nijmegen, 2000.
URL citeseer.ist.psu.edu/article/jacobs00formalisation.html
[14] Bart Jacobs, Hans Meijer y Erik Poll. VerifiCard: A European Project for Smart Card
Verification. Newsletter 5 of the Dutch Association for Theoretical Computer Science (NVTI),
2001.
URL http://www.cs.kun.nl/~bart/PAPERS/nvti01.ps.Z
[15] Bill Joy, James Gosling, Guy Steele y Gilad Bracha. The Java Language Specification. Addison
29
Wesley Professional, tercera edición, 2005.
URL http://java.sun.com/docs/books/jls/third_edition/html/j3TOC.html
[16] Murat Karaorman, Urs Hölzle y John Bruno. jcontractor: A reflective java library to support
design by contract. En P. Cointe, editor, Meta-Level Architectures and Reflection, 2nd Int’l
Conf. Reflection, tomo 1616 de LNCS, páginas 175–196. Springer Verlag, Berlin, Alemania,
1999.
URL http://www.cs.ucsb.edu/labs/oocsb/papers/TRCS98-31.pdf
[17] Gary Leavens y Yoonsik Cheon. Design by Contract with JML, Enero 2005.
URL ftp://ftp.cs.iastate.edu/pub/leavens/JML/jmldbc.pdf
[18] Gary Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, Peter Müller
y Joseph Kiniry. JML Reference Manual, Julio 2005.
URL http://www.cs.iastate.edu/~leavens/JML/jmlrefman/jmlrefman_toc.html
[19] Barbara Liskov y Jeannette Wing. Behavioral subtyping using invariants and constraints.
Informe Técnico CS99-156, School of Computer Science, Carnegie Mellon University, Julio
1999.
URL http://citeseer.ist.psu.edu/liskov99behavioral.html
[20] Bertrand Meyer. Object-oriented Software Construction. Prentice Hall, 1988.
[21] Carroll Morgan. On the Refinement Calculus. Springer-Verlag, 1994.
[22] John Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. En Symposium on Logic in Computer Science, 2002. 29. 2002.
URL http://citeseer.ist.psu.edu/reynolds02separation.html
30
[23] Rational Software. Rational unified process: Best practices for software development teams.
White Paper, diciembre 2003.
URL http://www-106.ibm.com/developerworks/rational/library/253.html
[24] Ascánder Suárez. Implementación de GCL: GaCeLa. Caracas, Venezuela, 2004.
URL http://gacela.labf.usb.ve/GCLWiki/Wiki.jsp
[25] Paul Szymkowiak. Testing: The rup philosophy. The Rational Edge, Febrero 2003.
[26] Joachim van den Berg y Bart Jacobs. The LOOP compiler for Java and JML. Lecture Notes
in Computer Science, 2031:299, 2001.
URL http://citeseer.ist.psu.edu/vandenberg01loop.html
Glosario
Aliasing: fenómeno que ocurre cuando un objeto tiene más de un nombre, y que suele traer
como consecuencia cambios inesperados en la instancia; un caso particular de esto sucede
cuando un objeto es referenciado por más de un apuntador.
Efecto de borde (o secundario): consecuencia inesperada y generalmente indeseada, se considera un efecto extra de la ejecución de una acción o la evaluación de una expresión; en
particular, el caso de modificar variables mientras se evalúan expresiones correspondientes
a la especificación.
Extender gramática: crear una gramática cuyo lenguaje asociado sea un superconjunto del
asociado a la gramática original; la nueva presenta ciertas facilidades adicionales que la
anterior no tenı́a.
Invariante: 1. I. de ciclo aserción que se debe cumplir al inicio y al final de cada vuelta de
un ciclo 2. I. de clase aserción que se debe cumplir en cada uno de los puntos visibles de
una clase (al inicio y final de los métodos y al final de los constructores).
Precondición: aserción que se debe cumplir al inicio de un método.
Predicado: expresión booleana.
Postcondición: aserción que se debe cumplir al final de un método.
31
32
Smart Card: tarjetas que tienen un pequeño procesador, cuya funcionalidad es permitir el
acceso a diversos servicios, alguno de los cuales puede requerir un alto grado de confidencialidad y seguridad.
Apéndice A
Código de los casos de prueba para JUnit
Estos casos de prueba se usaron para evaluar una versión temprana del reconocedor, la cual
sólo reconocia expresiones y además de reconocerlas, permitı́a la posibilidad de evaluarlas.
A continuación se presenta el código de los casos de prueba relativos a la lista de variables:
import junit.framework.*;
public class ExprBooleanaTest extends TestCase {
private ExprBooleanaConstante verdadera;
private ExprBooleanaConstante falsa;
private ExprBooleanaIdentif x1, x2, x3, x4;
public static void main(String args[]) {
junit.textui.TestRunner.run(suite());
}
public static Test suite() {
TestSuite suite = new TestSuite(ExprBooleanaTest.class);
return suite;
}
public void setUp() {
verdadera = new ExprBooleanaConstante(true);
falsa = new ExprBooleanaConstante(false);
x1 = new ExprBooleanaIdentif("x1");
x2 = new ExprBooleanaIdentif("x2");
x3 = new ExprBooleanaIdentif("x3");
x4 = new ExprBooleanaIdentif("x4");
}
33
34
public void testListaVar1() throws ExcepcionIdentifNoEnTabla {
ExprBooleana expresion, esperada;
expresion = new ExprBooleanaBinaria(’&’, verdadera, falsa);
esperada = falsa;
assertTrue(expresion.evaluar(new TablaIdentif())==esperada.evaluar(new TablaIdentif()));
}
public void testListaVar2() throws ExcepcionIdentifNoEnTabla {
ExprBooleana expresion, esperada;
expresion = new ExprBooleanaBinaria(’y’, new ExprBooleanaBinaria(’y’, verdadera, x1),
new ExprBooleanaUnaria(’!’, x2));
esperada = verdadera;
TablaIdentif tabla = new TablaIdentif();
tabla.asignar(new Entrada("x1", true));
assertTrue(expresion.evaluar(tabla)==esperada.evaluar(tabla));
}
public void testListaVar3() throws ExcepcionIdentifNoEnTabla {
ExprBooleana expresion, esperada;
expresion = new ExprBooleanaBinaria(’y’, new ExprBooleanaBinaria(’y’, verdadera, x1),
new ExprBooleanaUnaria(’!’, x2));
esperada = verdadera;
TablaIdentif tabla = new TablaIdentif();
tabla.asignar(new Entrada("x1", true));
tabla.asignar(new Entrada("x2", false));
assertTrue(expresion.evaluar(tabla)==esperada.evaluar(tabla));
}
public void testListaVar4() throws ExcepcionIdentifNoEnTabla {
ExprBooleana expresion, esperada;
expresion = new ExprBooleanaBinaria(’^’, verdadera, falsa);
esperada = verdadera;
TablaIdentif tabla = new TablaIdentif();
tabla.asignar(new Entrada("x1", true));
tabla.asignar(new Entrada("x2", false));
tabla.asignar(new Entrada("x3", true));
assertTrue(expresion.evaluar(tabla)==esperada.evaluar(tabla));
}
public void testListaVar5() throws ExcepcionIdentifNoEnTabla {
ExprBooleana expresion, esperada, auxiliar;
35
auxiliar = new ExprBooleanaBinaria(’y’, new ExprBooleanaUnaria(’!’, x1), falsa);
expresion = new ExprBooleanaBinaria(’o’, new ExprBooleanaUnaria(’!’, auxiliar), x2);
esperada = verdadera;
TablaIdentif tabla = new TablaIdentif();
tabla.asignar(new Entrada("x1", true));
tabla.asignar(new Entrada("x2", false));
tabla.asignar(new Entrada("x3", true));
tabla.asignar(new Entrada("x4", true));
assertTrue(expresion.evaluar(tabla)==esperada.evaluar(tabla));
}
public void testListaVar6() throws ExcepcionIdentifNoEnTabla {
ExprBooleana expresion, esperada, auxiliar;
auxiliar = new ExprBooleanaBinaria(’&’, x1, x2);
expresion = new ExprBooleanaBinaria(’o’, auxiliar, falsa);
esperada = falsa;
TablaIdentif tabla = new TablaIdentif();
tabla.asignar(new Entrada("x1", true));
tabla.asignar(new Entrada("x2", true));
tabla.asignar(new Entrada("x1", false));
assertTrue(expresion.evaluar(tabla)==esperada.evaluar(tabla));
}
}
Apéndice B
Formato de los casos de prueba de TestJCR
El formato del archivo es:
<nombreDelPrograma>
%
<datosDeEntrada0>
#
<resultados0>
%
<datosDeEntrada1>
#
<resultados1>
...
<datosDeEntradaN>
#
<resultadosN>
@
Se compilará y se ejecutará muchas veces el programa llamado <nombreDelPrograma>, y se le
pasará en cada ocasión los <datosDeEntrada> correspondientes y se verificará que se produzcan
los <resultados> esperados.
Nota0: si los resultados se reflejan en una estructura de datos compleja, previamente se determinará en que formato se representarán.
Nota1: esto fácilmente se usa para programas que lean los datos de entrada por entrada estándar e imprima por salida estándar los de salida, pero es análogo su uso para programas que
interactúan con archivos, leyendo y escribiendo respectivamente datos de entrada o salida.
36
Apéndice C
Programas en JML
C.1.
Programa tipo Algoritmos I: Factorial
/**
* Devuelve el valor correspondiente al factorial del entero pasado como par’ametro
*
* @param i valor entero al que se le calcularar’a el factorial
* @return el valor del factorial de i
*/
/*@
@ requires i >= 0;
@ ensures (\result == (\product int k; 1 <= k && k <= i; k));
@*/
public static int fact(int i) {
if (i == 0) {
return 1;
} else {
return (i * fact(i - 1));
}
}
C.2.
Programa tipo Algoritmos I: Ordenamiento Burbuja
/**
* Dado un arreglo, devuelve el arreglo ordenado ascendentemente correspondiente
* a los valores que conten’ia el original.
*
* @param a arreglo de valores a ordenar
*
* @return el arreglo ordenado
*/
37
38
/*@
@ ensures
@
(arreglo.length == \old(arreglo.length))
@
&&
@
(\forall int i
@
;0 <= i && i < arreglo.length
@
;(\num_of int j; 0 <= j && j < arreglo.length; arreglo[i] == arreglo[j])
@
==
@
(\num_of int j; 0 <= j && j < \old(arreglo.length); arreglo[i] == \old(arreglo[j]))
@
)
@
&&
@
(\forall int i; 0 <= i && i < arreglo.length - 1; arreglo[i] <= arreglo[i + 1]);
@*/
public static void ordenar(int arreglo[]) {
int i = 0;
/*@
@ loop_invariant
@
(0 <= i && (arreglo.length > 0 ==> i <= arreglo.length - 1))
@
&&
@
(\forall int l
@
;arreglo.length - 1 - i <= l && l < arreglo.length - 1
@
;arreglo[l] <= arreglo[l + 1]
@
)
@
&&
@
(\forall int m, l
@
;0 <= m && m <= arreglo.length - 1 - i && arreglo.length - 1 - i < l && l <arreglo.length
@
;arreglo[m] <= arreglo[l]
@
);
@ decreasing (arreglo.length - i);
@*/
for (; i < arreglo.length - 1; i++) {
int j = 0;
/*@
@ loop_invariant
@
(0 <= j && j <= arreglo.length - 1 - i)
@
&&
@
(\forall int k; 0 <= k && k < j; arreglo[k] <= arreglo[j]);
@ decreasing (arreglo.length - 1 - i - j);
@*/
for (; j < arreglo.length - 1 - i; j++) {
39
if (arreglo[j] > arreglo[j + 1]) {
swap(arreglo, j, j + 1);
}
}
}
}
C.3.
Programa tipo Algoritmos II: TAD Diccionario
import java.util.Vector;
class Diccionario {
private /*@ spec_public @*/ Vector claves;
private /*@ spec_public @*/ Vector valores;
private /*@ spec_public @*/ int tam;
/*@
@ invariant 0 <= tam
@
&&
@
(\forall int i, j
@
;0 <= i && i < tam && 0 <= j && j < tam
@
;claves.elementAt(i).equals(claves.elementAt(j)) ==> i == j
@
);
@*/
//@ ensures tam == 0 && valores.size() == 0 && claves.size() == 0;
public Diccionario() {
tam = 0;
claves = new Vector();
valores = new Vector();
}
/*@
@ requires !(conocida(clave));
@ ensures
((String) claves.elementAt(tam - 1)).equals(clave)
@
&&
@
((String) valores.elementAt(tam - 1)).equals(valor)
@
&&
@
\old(tam) + 1 == tam
@
&&
@
(\forall int i
@
;0 <= i && i < tam - 1
40
@
;((String) claves.elementAt(i)).equals((String) \old(claves).elementAt(i))
@
&&
@
((String) valores.elementAt(i)).equals((String) \old(valores).elementAt(i))
@
);
@*/
public void agregar(String clave, String valor) {
claves.add(clave);
valores.add(valor);
tam++;
}
/*@
@ requires (conocida(clave));
@ ensures (\forall int i
@
;0 <= i && i < posicion(clave)
@
;((String) claves.elementAt(i)).equals((String) \old(claves.elementAt(i)))
@
)
@
&&
@
(\forall int i
@
;posicion(clave) <= i && i < tam
@
;((String) claves.elementAt(i)).equals((String) \old(claves.elementAt(i + 1)))
@
)
@
&&
\old(tam) - 1
== tam;
@*/
public void eliminar(String clave) {
valores.remove(claves.indexOf(clave));
claves.remove(claves.indexOf(clave));
tam--;
}
/*@
@ requires conocida(clave);
@ ensures (\exists int i
@
;0 <= i && i < tam
@
;claves.elementAt(i).equals(clave)
@
&&
@
\result.equals((String) valores.elementAt(i))
@
);
@*/
public /*@ pure @*/ String obtener(String clave) {
return((String) valores.elementAt(claves.indexOf(clave)));
41
}
//@ ensures \result == (\exists int i; 0 <= i && i < tam; claves.elementAt(i).equals(clave));
public /*@ pure @*/ boolean conocida(String clave) {
return(claves.contains(clave));
}
//@ ensures \result == (tam == 0);
public /*@ pure @*/ boolean esVacio() {
return(tam == 0);
}
/*@
@ requires conocida(clave);
@ ensures claves.elementAt(\result) == clave;
@*/
private /*@ pure spec_public @*/ int posicion(String clave) {
return(claves.indexOf(clave));
}
}
Apéndice D
Detalles de Implementación
El esquema de análisis sintáctico LALR(1), que utiliza la herramienta Claire, generaba conflictos con la gramática propuesta para JCR, y por tanto se tuvo que recurrir a una modificación
del lenguaje que, imponiendo restricciones extra al lenguaje, logra eliminar las ambigüedades
existentes bajo este esquema. A continuación se presentan las concesiones que se tuvieron que
hacer:
Prohibir los comentarios entre @ e interface en la declaración de un tipo de anotación-Java,
esto debido a que al punto de estar reconociendo los modificadores que puede tener esta
declaración y que el próximo terminal sea un @ no se puede determinar si es una anotación
ya creada o que se está declarando el tipo de anotación.
Agrupar en una regla varios no-terminales opcionales, y usarla en algunas reglas donde
algunos de esos no terminales no deberı́an aparecer. Se debe a que al tener elementos en
común y ser opcionales no se puede determinar a cuál de las posibles reglas corresponde.
Esta limitación sin embargo puede ser solucionada a través del uso de atributos en el tipo
de retorno de esa regla que indiquen cuáles no terminales se reconocieron y dando un error
en caso de que se reconozca alguno que no corresponde a ese punto de reconocimiento.
42
43
Las especificaciones de los métodos y constructores se deben colocar luego del encabezado.
Esto limita las opciones de JML de poder colocarlo al inicio o al final del encabezado.
Esto se debe a que los posibles modificadores del encabezado causan confictos con la regla
privacy que es parte de los no-terminales de la regla model_program, la cual es una posible
especificación.
Obligar a tener la separación de rango y predicado en las cuantificaciones, ası́ el rango sea
vacı́o. Esto debido a que, teniendo todo esto opcional, se generan conflictos al momento de
reconocer una expresión: no se identifica si se está reconociendo el rango o el predicado (y
no habı́a rango).
Inclusión de una serie de reglas adicionales sobre las expresiones que evitan que éstas vayan
al no-terminal name antes de que sea la última opción, ya que con la gran cantidad de reglas
que van a name, no se está seguro de a cuál de tantas corresponde.
Eliminar la coma opcional en las reglas: element_value_array_initializer, enum_body,
array_initializer; ya que al estar ésta luego de una lista, no se puede determinar con
certeza si la lista terminó o no.
Colocar información un poco repetitiva en la regla explicit_constructor_invocation
y no hacer buen uso de las macros disponibles, esto debido a que, si se utilizan para
mejorar esto, se crean conflictos con la regla primary_no_new_array, por el no-terminal
opt(type_arguments).
No permitir colocar una etiqueta (name :) en la regla possibly_annotated_loop, ya que
esto generı́a confusión con la regla labeled_statement.
44
Además de las anteriores concesiones, también se cambiaron otros aspectos. A pesar de que
estos cambios se hicieron principalmente por no lograr el reconocimiento por limitaciones de la
herramienta, se determinó que conservar estos cambios es más conveniente que tener la versión
original de JML. Esos aspectos son los siguientes:
No permitir el tipo arreglo como resultado de la creación de un conjunto.
No utilizar el modificador weakly de JML, hasta que no se compruebe que es conveniente
tener subclases que no sean behavioral subtypes
Y por falta de documentación no se incluyeron las reglas normal_spec_clause y redundant_spec, la primera de ellas por no contar con la especificación de cómo reducir ese no terminal
y la segunda por depender de la primera.
Anexo 1
Ejemplo de programa en JContractor
Programa: PriorityQueue
package edu.ucsb.ccs.jcontractor.examples.heap;
/**
* Abstract description of a datastructure that allows easy access to
* its largest element.
*
* @author Parker Abercrombie
*
* @invariant size () >= 0
* @invariant isFull() implies !isEmpty()
* @invariant isEmpty() implies !isFull()
*/
public interface PriorityQueue {
/**
* Is the queue empty?
*
* @return <code>true</code> if there are no items in the queue,
*
otherwise <code>false</code>.
*/
public boolean isEmpty ();
/**
* Is the queue full?
*
* @return <code>true</code> if no more items may be added to the
*
queue.
*/
public boolean isFull ();
/**
45
46
* Get the largest element in the queue.
*
* @return the largest element in the queue.
*
* @pre !isEmpty ()
*
* @post return != null
* @post size() == size()@pre
*/
public Comparable item ();
/**
* Remove all elements from the queue.
*
* @post isEmpty ()
*/
public void clear ();
/**
* Get the number of elements in the queue.
*
* @return the number of elements in the queue.
*
* @post return >= 0
*/
public int size ();
/**
* Determine how many times ‘key’ appears in the queue.
*
* @param key the item to search for.
*
* @return the number of times <code>key</code> appears in the
* queue.
*/
public int occurences (Comparable key);
/**
* Add an item to the queue.
*
* @param newItem the item to add.
*
* @pre newItem != null
* @pre !isFull()
*
* @post !isEmpty ()
* @post size () == size()@pre + 1
47
* @post occurences (newItem) == occurences(newItem)@pre + 1
*/
public void put (Comparable newItem);
/**
* Remove and return the largest item in the queue.
*
* @return the item that was removed.
*
* @pre !isEmpty ()
*
* @post !isFull()
* @post size() == size()@pre - 1
* @post return == item()@pre
* @post occurences (return) == occurences(item())@pre - 1
* @post return != null
*/
public Comparable remove ();
}
Programa que contiene los contratos de la clase PriorityQueue
package edu.ucsb.ccs.jcontractor.examples.heap;
public abstract class PriorityQueue_CONTRACT implements PriorityQueue {
protected boolean item_Precondition () {
return !isEmpty();
}
protected boolean item_Postcondition (Comparable RESULT) {
return (RESULT != null);
}
protected boolean clear_Postcondition (boolean RESULT) {
return isEmpty();
}
protected boolean size_Postcondition (int RESULT) {
return RESULT >= 0;
}
protected boolean put_Precondition (Comparable newItem) {
return (newItem != null) && !isFull();
}
48
protected boolean put_Postcondition (Comparable newItem,
Void RESULT) {
return !isEmpty();
}
protected boolean remove_Postcondition (Comparable RESULT) {
return !isFull() && (RESULT != null);
}
}
Códigos de Parker Abercrombie, distribuidos con la última versión de JContractor
(jcontractor-0.1/src/edu/ucsb/ccs/jcontractor/examples/heap).
Anexo 2
Ejemplo de programa en JML
Programa: LinearSearch
// @(#)$Id: LinearSearch.java,v 1.4 2005/02/17 17:05:32 leavens Exp $
// Copyright (C) 1998, 1999 Iowa State University
// This file is part of JML
// JML is free software; you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2, or (at your option)
// any later version.
// JML is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
See the
// GNU General Public License for more details.
// You should have received a copy of the GNU General Public License
// along with JML; see the file COPYING.
If not, write to
// the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
package org.jmlspecs.samples.misc;
/** A linear search component, intended to demonstrate verification in
* JML specifications.
This class has two abstract methods that
* describe the search, which need to be filled in to instantiate
* it.
The formulation of the search and the verification
* is based on Edward Cohen’s book
* <cite>Programming in the 1990s</cite> (Springer-Verlag, 1990).
* @author Gary T. Leavens
*/
public abstract class LinearSearch
{
49
50
/** The function that describes what is being sought. */
//@ requires j >= 0;
public abstract /*@ pure @*/ boolean f(int j);
/** The last integer in the search space, this describes the
* domain of f, which goes from 0 to the result.
*/
//@ ensures 0 <= \result;
//@ ensures (\exists int j; 0 <= j && j <= \result; f(j));
public abstract /*@ pure @*/ int limit();
/** Find a solution to the searching problem. */
/*@ public normal_behavior
@
requires (\exists int i; 0 <= i && i <= limit(); f(i));
@
assignable \nothing;
@
ensures \result == (\min int i; 0 <= i && f(i); i);
@*/
public int find() {
int x = 0;
//@ maintaining 0 <= x && (\forall int i; 0 <= i && i < x; !f(i));
//@ decreasing limit() - x;
while (!f(x)) {
/*@ assert 0 <= x && !f(x)
@
&& (\forall int i; 0 <= i && i < x; !f(i));
@*/
//@ hence_by (* arithmetic *);
/*@ assert 0 <= (x+1)-1 && !f((x+1)-1)
@
&& (\forall int i; 0 <= i && i < (x+1)-1; !f(i));
@*/
x = x + 1;
/*@ assert 0 <= x-1 && !f((int)(x-1))
@
&& (\forall int i; 0 <= i && i < x-1; !f(i));
@*/
//@ hence_by (* arithmetic, constant term rule *);
/*@ assert 0 <= x && (\forall int i; i == x-1; !f(i))
@
&& (\forall int i; 0 <= i && i < x-1; !f(i));
@*/
//@ hence_by (* joining the range *);
/*@ assert 0 <= x &&
@
(\forall int i; (0 <= i && i < x-1) || i == x-1; !f(i));
@*/
//@ hence_by (* arithmetic *);
//@ assert 0 <= x && (\forall int i; 0 <= i && i < x; !f(i));
}
/*@ assert 0 <= x && f(x)
@
@*/
&& (\forall int i; 0 <= i && i < x; !f(i));
51
//@ hence_by (* definition of \min *);
//@ assert x == (\min int i; 0 <= i && f(i); i);
return x;
}
}
Código de Gary Leavens, distribuido con la versión actual de JML
(JML/org/jmlspecs/samples/misc/LinearSearch.java).