Prácticas TP, 16/03/2005

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

  1. Organizarse en grupos de 2 personas. Cada grupo "competirá" más tarde con otro de los grupos.

  2. 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).

  3. 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.

  4. 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;