PDF de programación - Introducción al lenguaje de especificación JML

Introducción al lenguaje
de especificación JML

Elena Hernández Pereira
Óscar Fontenla Romero

Tecnología de la Programación

― Octubre 2006 ―

Departamento de Computación
Facultad de Informática
Universidad de A Coruña

Bibliografía

JML Home Page:

http://www.jmlspecs.org

Documento sobre diseño preliminar de JML:

http://www.cs.iastate.edu/~leavens/JML/prelimdesign/pr

elimdesign_toc.html
Manual de referencia:

http://www.cs.iastate.edu/~leavens/JML/jmlrefman/

Código libre JML y herramientas (incluye el

compilador):
http://sourceforge.net/projects/jmlspecs/

Introducción a JML

2

1

Introducción (I)

JML (Java Modeling Language): lenguaje de

especificación para programas Java

Las especificaciones se introducen en los ficheros

fuente de Java

Las especificaciones JML hacen una descripción formal

del comportamiento de clases y métodos

Añadir especificaciones JML a un programa ayuda a:

Comprender qué función debe realizar un método o una

clase

Encontrar errores en los programas: comprueba si un

método cumple su especificación cada vez que se ejecuta

Introducción a JML

3

Empezando a especificar (I)

Aserción o anotación: cláusula lógica insertada en un

programa

Objetivo de una aserción: representar una condición que

debe ser cierta en un punto del programa

Esta condición puede ser una condición típica de Java,

escrita usando los operadores lógicos && y ||

La cláusula de JML assert sirve para indicar estas

condiciones o aserciones en cualquier lugar de un programa
Si la condición no fuese cierta entonces el programa se
detiene y se visualizara un error en tiempo de ejecución
indicando que dicha aserción no se cumple.

Introducción a JML

4

2

Empezando a especificar (II)

Ejemplo:

// Este código almacena en z el mayor de x e y
if (x >= y)
else
//@ assert z >= x && z >= y;

z = x;
z = y;

La condición que debe ser cierta se indica a continuación de
la cláusula assert, y debe estar terminada con el carácter ;

Delante de la cláusula aparecen los caracteres //@ que

indican al compilador que la línea contiene una cláusula de
JML

¿Es suficiente la condición del assert?:

NO

Introducción a JML

Empezando a especificar (III)

Si se cambia el código por:

// Este código almacena en z el mayor de x e y
z = x*x + y*y;
//@ assert z >= x && z >= y;

La condición se haría cierta, y sin embargo z no

contiene el mayor de x e y

¿Cómo mejorar la aserción para solucionar el

problema?

Introducción a JML

5

6

3

Empezando a especificar (IV)

Posible solución:

// Este código almacena en z el mayor de x e y
if (x >= y)
else

z = x;
z = y;

//@ assert z >= x && z >= y && (z == x || z == y);

Hay dos aserciones que reciben un nombre particular:

Aserción precondición: condición que debe cumplirse

para que un método pueda ejecutarse

Aserción postcondición: condición que debe cumplirse al

acabar la ejecución de un método

Introducción a JML

Empezando a especificar (V)

Ejemplo: para poder hacer una operación de división

Precondición: divisor distinto de cero
Postcondición: dividendo == divisor*cociente + resto

Clásulas JML para la precondición y postcondición de

un método: requires y ensures
Deben ir antes de la declaración del método

JML recoge en la variable \result el valor devuelto

por el método

Introducción a JML

7

8

4

Empezando a especificar (VI)

Ejemplo: postcondición para el método del máximo

/* Método maximo:

Devuelve el mayor de x e y */

//@ ensures \result>= x && \result>= y && (\result == x || \result == y);
public static int maximo(int x, int y)
{

int z;
if (x >= y)
else

z = x;
z = y;
return z;

}

Introducción a JML

9

Empezando a especificar (VII)

También es posible indicar varias precondiciones o

postcondiciones: todas ellas se deben cumplir

Ejemplo

/* Método maximo: Devuelve el mayor de x e y */
//@ requires true;
//@ ensures \result >= x && \result >= y;
//@ ensures \result == x || \result == y;
public static int maximo(int x, int y)
{

int z;
if (x >= y)
z = x;
else
z = y;
return z;

}

Introducción a JML

10

5

Empezando a especificar (VIII)

Si hay varias líneas de aserciones se pueden emplear

las marcas /*@ y @*/

Ejemplo:

/* Método maximo: Devuelve el mayor de x e y */
/*@ requires true;

@ ensures \result >= x && \result >= y;
@ ensures \result == x || \result == y;
@*/

public static int maximo(int x, int y)
{

int z;
if (x >= y)
z = x;
else
z = y;
return z;

}

Introducción a JML

11

Expresiones de especificación (I)

Expresión de especificación: expresión similar a un

predicado de lógica que se evalúa a cierto o falso
Permiten describir condiciones que deben ser ciertas en

determinados puntos durante la ejecución de un
programa

Permiten especificar el comportamiento de los métodos y

también de la clase

Se puede indicar con una condición que utilice:

Los operadores lógicos de Java como &&, ||, !, etc.,
Los operadores de comparación ==, !=, <, <=, etc.
Cuantificadores más comunes (universal, existencial, etc.)
Otros operadores lógicos

Introducción a JML

12

6

Expresiones de especificación (II)

Operadores y cuantificadores:

Operadores

Cuantificadores

==>
<==
<==>
<=!=>
\forall
\exists
\sum
\product
\num_of
\max
\min

Implicación
Contraimplicación
Equivalencia
No equivalencia
Para todo
Existe
Suma
Producto
Número de
Máximo
Mínimo

Introducción a JML

13

Expresiones de especificación (III)

Todos los cuantificadores tienen la misma sintaxis:

Definición de una variable ligada
Rango de la variable
Expresión sobre la que se aplica el cuantificador

Ejemplos:

Expresión

(\sum int I; 0 <= I && I < 5; I)

(\product int I; 0 < I && I < 5; I)

(\max int I; 0 <= I && I < 5; I)

(\min int I; 0 <= I && I < 5; I-1)

(\num_of int I; 0 <= I && I < 5; I*2 < 6)

Equivale a

0 + 1 + 2 + 3 + 4

1 * 2 * 3 * 4

4

-1

3

Introducción a JML

14

7

Expresiones de especificación (IV)

JML también define dos seudovariables que pueden
ser utilizadas en las postcondiciones de los métodos:
\result: valor devuelto por el método
\old(E): valor que tomaba la expresión E al comenzar la

ejecución del método

En las aserciones no está permitido:

Utilizar operadores que modifiquen variables: ++, --, =,

+=, y todos los operadores que contienen =

Llamadas a métodos que modifiquen variables no

locales: métodos con efectos laterales

Introducción a JML

15

Expresiones de especificación (V)

Ejercicio 1: especificación de un método que devuelve la

suma de todos los elementos de un array de enteros

Precondiciones:

El array no es nulo (está creado)

Postcondiciones:

Resultado método =

1

N

∑−

i

=

0

array

i
][

Los elementos del array no se modifican

Introducción a JML

16

8

Expresiones de especificación (VI)

Ejercicio 1: especificación de un método que devuelve la

suma de todos los elementos de un array de enteros

/*@

@ requires array != null;
@ ensures \result == (\sum int I; 0 <= I && I < array.length; array[I]);
@ ensures (\forall int I; 0 <= I && I < array.length;
@ array[I] == \old(array[I]));
@*/

public static int sumaDeArray(int[] array) {

// Cuerpo del método

}

Introducción a JML

17

Expresiones de especificación (VII)

Ejercicio 2: especificación de un método que inserte un elemento

en una posición dada de una matriz sin modificar el resto de
elementos

/*@ requires matriz != null;

@ requires Posx >= 0 && Posy >= 0;
@ requires Posx < matriz.length && Posy < matriz[0].length;
@ ensures (\forall int I; 0 <=I && I < matriz.length;
@ (\forall int J; 0<=J && J < matriz[0].length;
(I==Posx && J==Posy && matriz[I][J]==Dato) ||
@
@
matriz[I][J]==\old(matriz[I][J]) ));
@*/

public static int insertarElemento(int matriz[][], int Posx, int Posy, int Dato)
{

// Cuerpo del método

}

¿Es correcta esta especificación?:

NO

Introducción a JML

18

9

Expresiones de especificación (VIII)

Ejercicio 2 (una de las posibles soluciones correctas):

especificación de un método que inserte un elemento en una
posición dada de una matriz sin modificar el resto de elementos

/*@ requires matriz != null;

@ requires Posx >= 0 && Posy >= 0;
@ requires Posx < matriz.length && Posy < matriz[0].length;
@ ensures matriz[Posx][Posy] == Dato &&
@
@ (\forall int J; 0<=J && J < matriz[0].length;
@
@ ));
@*/

(\forall int I; 0 <=I && I < matriz.length;

(I!=Posx || J!=Posy) ==> matriz[I][J]==\old(matriz[I][J])

public static int insertarElemento(int matriz[][], int Posx, int Posy, int Dato)
{

// Cuerpo del método

}

Introducción a JML

19

Expresiones de especificación (IX)

Comentarios para aclarar el objetivo de cada aserción:

(* esto es un comentario *)
Son tratados como una aserción más, por tanto deben ir unidas

a otras aserciones utilizando el operador &&

Siempre serán evaluadas como ciertas
Ejemplo:

/*@ requires array != null;

@ ensures (* devuelve la suma de todos los elementos del array *)
@ && \result == (\sum int I; 0 <= I && I < array.length; array[I]);
@ ensures (* no modifica el array *)
@ && (\forall int I; 0 <= I && I < array.length;
@ array[I] == \old(array[I]));
@*/

Introducción a JML

20

10

Expresiones de especificación (X)

Ejercicio 3: especificación de un método que intercambie