Ejercicio 2
Se desea construir una clase llamada
VectorDinamico para gestionar
un vector cuyo
tamaño aumenta según se van añadiendo objetos. El
vector depende de un parámetro
tamBloque que indica en
cuánto crece el espacio disponible una vez que hemos agotado el
actual. Como ejemplo, si
tamBloque
=5, y añadimos uno a uno al vector los elementos "a", "b", "c",
"d",
"e", "f", se produciría la secuencia de estados:
[ - , - , - , - , - ] inicialmente hay 0
elementos, pero espacio para 5
[ a , - , - , - , - ]
[ a , b , - , - , - ]
[ a , b , c , - , - ]
[ a , b , c , d , - ]
[ a , b , c , d , e ]
Hemos agotado el primer bloque de 5. Ahora reservamos un array de otros
5 elementos más (10 en total) y copiamos los elementos
anteriores, más
el nuevo a insertar
[ a , b , c , d , e , f , - , - , - , - ]
Tenemos ahora 6 elementos y espacio total para 10.
public class VectorDinamico {
// Constructores -------------
/** Crea un nuevo vector con tamaño de bloque tamBloque. */ public VectorDinamico(int tamBloque);
/** Crea un nuevo vector con tamaño de bloque 5, por defecto. */ public VectorDinamico();
// Modificadores ------------
/** Añade el elemento x al final del vector actual. */ public añade(Object x); /** Inserta el elemento x en la posición i del vector actual, * desplazando en una posición a la derecha todos los elementos * desde i hasta el último. */ public añade(int i,Object x); /** El elemento de la posición i pasa a ser x. No cambia el * número total de elementos. */ public void fijarElemento(int i,Object x);
// Consulta -----------------
/** Devuelve la longitud del vector, es decir, el número de * elementos almacenados. */ public int longitud(); /** Devuelve el i-ésimo elemento del vector.*/ public Object elemento(int i);
/** Devuelve la primera posición por la izquierda en la que * aparece el elemento x. Si x no estuviera en el array, entonces * devuelve -1 sin más. Para comparar elementos debe usarse * el método equals. */ public int indice(Object x);
/** Imprime el contenido del vector en un string. */ public String toString();
} // class VectorDinamico
|
Pasos a seguir
- Organizarse en grupos de 2 personas. Cada grupo
"competirá" más tarde con otro de los grupos.
- Al construir la clase, el grupo deberá no sólo
programar
en java sus métodos, sino también añadir aquellas
aserciones
JML que considere necesarias (precondiciones, postcondiciones,
invariantes
de clase, etc).
- Una vez finalizado el trabajo, los 2 grupos se
intercambiarán
los programas, con el siguiente objetivo. Intentaremos introducir
errores
en el código del programa sin modificar las aserciones que
el otro grupo haya incluido. Así, podemos cambiar libremente el
código de cualquier método,
convirtiéndolo en erróneo. También podemos hacer
un
uso indebido o no esperado del método en la llamada desde main.
En ambos casos, nuestro objetivo es introducir un erro que no sea
detectado por las aserciones JML. Como ejemplo, supongamos que
tenemos:
//@ ensures
\result>=y && \result>=x;
public static int maximo(int x, int y) {
if (x>=y) return x;
else return y;
}
|
Este método es correcto, pero no así su
postcondición.
Para demostrarlo, podemos modificarlo, por ejemplo, del siguiente modo:
//@ ensures
\result>=y && \result>=x;
public static int maximo(int x, int y) {
return x*x + y*y;
}
|
El resultado es incorrecto, y por tanto la postcondición
debería
controlarlo. Sin embargo, no obtenemos error de postcondición,
ya
que efectivamente, x*x + y*y es siempre mayor igual que x
y mayor o igual que y.
- Después de anotar los errores que hemos logrado
introducirle
al código sin que fueran controlados por las aserciones, ambos
grupos
intentarán buscar la forma de modificar estas últimas (si
es posible) para que esto no ocurra. En el caso anterior, la
postcondición debería incluir además:
//@ ensures \result==y
|| \result==x;
|