Cosa sono e come funzionano le invarianti di ciclo (loop invariants)
Le invarianti di ciclo sono un utile strumento che permette di provare la correttezza e la terminazione di un algoritmo che esegue al suo interno cicli. Seguendo una metodologia di sviluppo rigorosa, prima di implementare un metodo o una funzione dovremmo dichiarare le precondizioni e le postcondizi