----- 20/6/05 -----

> Per il "giro del cavallo" ho trovato il seguente invariante, ma non sono
> sicuro che sia corretto (a livello logico, perche' a livello sintattico
> funziona tutto senza che restituisca alcuna eccezione):
>
>   /** ( forall x : { 1 .. size } #
>         ( forall y : { 1 .. size } #
>           ( (chessBoard[x][y] > 0) && (chessBoard[x][y] < size*size) )
>           ) );
>   **/

Non e' chiaro quando si applica questo invariante, perche' nel corso del
processo risolutivo la scacchiera ha dei quadrati liberi: se un quadrato
libero e' individuato dal valore 0, allora la prima disuguaglianza dovrebbe
essere ">=" e non ">"; analogamente, alla fine la seconda disuguaglianza
dovrebbe essere "<=" e non "<" per il quadrato che e' stato raggiunto per
ultimo dal cavallo.

> Esisono altre condizioni da inserire nell'invariante di classe? Io non
> riesco a trovarne altre, perche' il resto del programma non mi sembra
> abbia invarianti.

Cosa piu' importante dell'osservazione fatta sopra, l'invariante proposto
(anche dopo gli aggiustamenti) dice solo che un quadrato, se e' raggiunto,
e' raggiunto dopo un numero di passi che va da 1 al numero complessivo di
posizioni disponibili, ma questo lascia spazio a diverse inconsistenze.

Bisognerebbe aggiungere asserzioni che esprimano ulteriori proprieta':

- Se due quadrati sono raggiunti ai passi m e n (> m), allora eistono
  quadrati che sono stati raggiunti in ciascuno dei passi intermedi
  fra m e n;

- Non ci possono essere due quadrati raggiunti allo stesso passo
  (ma ci possono essere un certo numero di quadrati liberi);

- Se due quadrati sono raggiunti nei passi k e k+1, allora il cavallo
  deve poter saltare direttamente dall'uno all'altro.

----- * -----