Changed lines 27-28 from:
// In un _qualunque_momento_ (invariante), la posizione di cima dello stack deve essere un numero positivo
to:
// In un _qualunque_momento_ (invariante), la posizione di cima dello stack deve
//essere un numero positivo
Changed lines 33-34 from:
// La chiamata al costruttore deve garantire la costruzione di uno stack di capacità n ed inizialmente vuoto
to:
// La chiamata al costruttore deve garantire la costruzione di uno stack di capacità
//n ed inizialmente vuoto
Changed lines 50-51 from:
// Alla fine dell'esecuzione di push, il numero e deve essere effettivamente inserito in cima allo stack
to:
// Alla fine dell'esecuzione di push, il numero e deve essere effettivamente
// inserito in cima allo stack
Changed lines 64-65 from:
// L'esecuzione del metodo pop richiede che lo stack sia non vuoto: +è una pre che dice che devo avere almeno un elemento
to:
// L'esecuzione del metodo pop richiede che lo stack sia non vuoto: +è una pre che
// dice che devo avere almeno un elemento
Changed lines 81-82 from:
//Al termine dell'esecuzione di resize, occorre che la capacità sia stata incrementata, ma gli elementi
to:
//Al termine dell'esecuzione di resize, occorre che la capacità sia stata
//incrementata, ma gli elementi
Changed lines 88-89 from:
// In realtà potrei anche scrivere ensures stack.length > old(stack.length), visto che le specifiche mi dicono solamente
to:
// In realtà potrei anche scrivere ensures stack.length > old(stack.length), visto
//che le specifiche mi dicono solamente
Added lines 1-103:
(:title LPS - Esercizi JML:)
%titolo%''':: 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 -> LinguaggiProgrammazioneSicurezza]]
