20200716

Page 1

Ingegneria del Software — SOLUZIONE DEL TEMA 16 luglio 2020 Esercizio 1 Si consideri la seguente specifica di una classe mutabile Buffer, che rappresenta un buffer di messaggi. Un messaggio `e un elemento della classe Message, specificata pi`u avanti. Il buffer permette l’inserimento di un messaggio in ultima posizione e la rimozione del messaggio in prima posizione (spostando di conseguenza tutti i messaggi rimanenti di una posizione). Il buffer pu`o contenere al massimo maxBytes() byte. p u b l i c c l a s s B u f f e r { / / C o s t r u i s c e un b u f f e r v u o t o che puo ’ c o n t e n e r e a l massimo maxBytes b y t e p u b l i c B u f f e r (i n t maxBytes ) ; / / @ensures ( * \ r e s u l t e ’ i l numero d i m e s s a g g i n e l b u f f e r *) p u b l i c / *@ pure @ * / i n t s i z e ( ) ; / / @ensures ( * \ r e s u l t e ’ i l messaggio i −esimo n e l b u f f e r s e 0 <=i <s i z e ( ) * ) . / / @signals ( I n d e x O u t O f B o u n d E x c e p t i o n e ) ( i<0 | | i >=s i z e ( ) ) ; p u b l i c / *@ pure @ * / Message g e t ( i n t i ) throws IndexOutOfBoundException ; / / @ensures ( * \ r e s u l t e ’ i l numero massimo d i b y t e che i l b u f f e r puo ’ c o n t e n t e r e *) p u b l i c / *@ pure @ * / i n t maxBytes ( ) ; / / @ensures ( * i n s e r i s c e un nuovo messaggio i n u l t i m a p o s i z i o n e *) / / @signals ( N u l l P o i n t e r E x c e p t i o n e ) ( * s e i l messaggio e ’ n u l l *) / / @signals ( B u f f e r F u l l E x c e p t i o n e ) / /@(* s e l ’ i n s e r i m e n t o d e l messaggio f a r e b b e s u p e r a r e i l massimo numero d i b y t e *) p u b l i c v o i d push ( Message m) throws N u l l P o i n t e r E x c e p t i o n , B u f f e r F u l l E x c e p t i o n ; / / @ensures ( * r e s t i t u i s c e e…