 | Question regarding Exercise 2 |
|
After taking a look at the Queue Class I cannot figure out the reason for the field N, since it is just used in the constructor ist should either be a constant or always represent the maximum number of elements the circular buffer currently supports. In the first case N should be declared final. In the second case resize should also update N. Consquently one could spezify N as follows: //@ private constraint N >= 0; //@ private constraint a != null ==> N == a.length Actually I'm not sure which approche to take. Perhaps there are other solutions as well. Thank you for any proposal. Sincerely Klaus |
 | Re: Question regarding Exercise 2 |
|
Dear Klaus, basically the first case applies. N is intended as a constant (even if not declared as final) that specifies the initial size of the array. Since only the constructor uses it, the only thing to say is that after the constructor call the size of the allocated array equals N (private behavior). In the specs of the other methods, N would not show up at all. Regards, Wolfgang |