LPS - Esercizi JML

 :: Esercizi JML ::

IntStack

La classe Java IntStack riportata sotto implementa la struttura dati STACK (una pila) per numeri interi tramite un array di dimensione finita ma che all’occorrenza può essere ridimensionato (vedi resize()) per aumentare la sua capacità di buffer.
Utilizzando JML, arricchire la classe IntStack secondo i principi del design by contract inserendo i seguenti invarianti:

• Il buffer deve essere non nullo;
• In un qualunque momento, la posizione di cima dello stack (il campo number) deve essere un numero positivo e non superare la capacità del buffer;

e le seguenti e pre-/post- condizioni:

• La chiamata al costruttore IntStack(n) deve garantire la creazione di uno stack di capacità n e inizialmente vuoto;
• Al termine dell’esecuzione del metodo push(e), il numero e deve essere stato effettivamente inserito in cima allo stack;
• L’esecuzione del metodo pop() richiede che lo stack sia non vuoto;
• Al termine dell’esecuzione del metodo pop(), il numero in cima allo stack è stato

cancellato;

• Al termine dell’esecuzione del metodo resize(), la capacità del buffer è stata

incrementata mantenendo il suo contenuto e lo stesso valore per la posizione di cima. Con un metodo main(), creare scenari validi/non validi (compilare con jmlc –Q).

class IntStack {

  // Il buffer deve essere non nullo
  /*@ non_null @*/ int[] stack; //buffer dello stack

  int number; //posizione di cima dello stack (prima posizione libera!)
  // In un _qualunque_momento_ (invariante), la posizione di cima dello stack deve 
  //essere un  numero positivo
  // e non superare la capacità dello stack
  //@ invariant number >= 0 && number <= stack.length;

  //Metodo costruttore: viene creato uno stack di capacità n ed inizialmente vuoto
  // La chiamata al costruttore deve garantire la costruzione di uno stack di capacità 
  //n ed inizialmente vuoto
  // Si tratta di una post
  /*@
  @ ensures stack.length == n && number == 0;
  @  
  @*/
  IntStack(int n) {
    stack = new int[n];
    number = 0;
  }

  //Restituisce true se lo stack è vuoto, false altrimenti
  boolean isempty() { 
    return number == 0; 
  }

  // Alla fine dell'esecuzione di push, il numero e deve essere effettivamente
  // inserito in cima allo stack
  /*@
  @ ensures (number == \old(number) +1) && (stack[\old(number)] == e);
  @*/

  void push(int e) {
    if (number == stack.length)
    resize();
    stack[number] = e;
    number = number+1;
  }

  //Cancella (e restituisce) un elemento dalla cima dello stack
  // L'esecuzione del metodo pop richiede che lo stack sia non vuoto: +è una pre che
  // dice che devo avere almeno un elemento
  /*@
  @ requires number > 0;
  @*/

  // Al termine dell'esecuzione di pop, il numero in cima allo stack deve essere cancellato
  /*@
  @ ensures (number == \old(number) - 1) && (\result == stack[number]);
  @*/

  int pop() {
    number = number-1;
    return stack[number];
  }

  //Aumenta la capacità di bufferizzazione dello stack
  //Al termine dell'esecuzione di resize, occorre che la capacità sia stata 
  //incrementata, ma gli elementi
  //devono essere mantenuti, e anche il valore di cima deve essere rimasto uguale
  /*@
  @ ensures stack.length == ((\old(stack.length) * 2) + 1) && (number == \old(number)) 
  @ && (\forall int i; 0 <= i && i < number; stack[i] == \old(stack[i]));
  @*/
  // In realtà potrei anche scrivere ensures stack.length > old(stack.length), visto   
  //che le specifiche mi dicono solamente
  // che la dimensione dello stack va incrementata, ma non di quanto
  void resize() {
    int s[] = new int[2*stack.length+1];
    for (int i=0; i<stack.length; i++)
      s[i] = stack[i];
    stack = s;
  }

  static public void main(String[] args) {
    IntStack S = new IntStack(10);
    S.push(20);
    S.push(30);
    int result = S.pop();
    System.out.println("Valore popped = " + result);
  }
}

---

Torna alla pagina di LPS