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 postcondizioni. Le loop invariant sono, in maniera analoga, le pre e post condizioni un ciclo.

Proviamo a dare una spiegazione intuitiva usando come esempio una funzione (Java) che esegue la somma degli elementi dell’ array dato in input:

public static int sum(int a[]) {
    int s = 0;
    for (int i = 0; i < a.length; i++) {
        // Invariante: "s" contiene la somma dei primi
        // "i" elementi dell'array:
        // s == a[0] + .. + a[i-1]
        // ed "i" è sempre minore della lunghezza di "a":
        // i < a.length
        s = s + a[i];
    }
    return s;
}

Il commento spiega l’invariante di questo ciclo. E’ interessante notare che:

  • Prima di eseguire la prima iterazione, s equivale a zero. Ed in effetti equivale alla somma dei primi 0 numeri.
  • Dopo la prima iterazione, s equivale a 0 + a[0], ovvero la somma del primo elemento.
  • Ripetendo le iterazioni per tutti gli elementi di a, alla fine s conterrà la somma di tutti gli “i” elementi di a.

Assumendo che la postcondizione di questo metodo era di voler trovare la somma di tutti gli elementi di a, abbiamo appena dimostrato tramite l’invariante di ciclo la correttezza di questa funzione.

Le loop invariant sono un ottimo strumento per dimostrare la correttezza di un loop, ma è bene ricordare che anche provarne la terminazione è importante. Per questo vengono utilizzate le loop variant.

Una loop variant definisce una quantità tendente a zero, tramite una variabile o una espressione che fa’ si che questa quantità decrementi ad ogni iterazione. Nell’esempio di sopra, i++ viene incrementato ad ogni iterazione, da questo possiamo quindi definire la nostra loop variant come: a.length - i. Questa quantità infatti, una volta terminato il ciclo, varrà zero. Questa espressione è direttamente collegata con la condizione definita nel for “i < a.length”. Questo vuol dire che, avendo dimostrato che la nostra loop variant è vera, il loop terminerà prima o poi.

Solitamente queste dimostrazioni vengono fatte per induzione sul numero di iterazioni. Le loop invariant quindi servono a dimostrare la correttezza dell’output ma le loop variant vengono usate per dimostrare che questo output verrà generato prima o poi.

Una loop invariant è uno statement (o un assioma) che:

  • E’ vera prima di qualunque iterazione (fase di inizializzazione)
  • E’ vera subito dopo aver eseguito il corpo del loop.
  • E’ vera dopo tutte le iterazioni.

Per capire meglio questa proprietà può essere utile immaginare un loop nel seguente modo:

while true {
   loop invariant
   if (guard) {
      corpo del loop
   } else {
      break
   }
}

Ad ogni iterazione, prima verifichiamo che l’invariante sia vera, poi decidiamo se eseguire il corpo del loop o uscire. E’ evidente che la loop invariant rimarrà vera una volta usciti da questo loop.

E’ interessante notare che nulla vieta all’invariante di ciclo di essere non valida nel corpo del loop. L’importante è prima e dopo ogni iterazione torni ad essere vera.

Una loop variant è invece una espressione di cui possiamo provare il decremento ad ogni iterazione del ciclo, tale per cui ad un certo punto assumerà un valore che renderà la condizione di iterazione (la condizione “guard” nell’if dell’esempio di sopra) falsa.

Perchè determinare le loop invariant di un ciclo?

Su un piano più filosofico: riuscire a scrivere la loop invariant di un ciclo, significa aver capito l’essenza del ciclo stesso. Non scriverlo, significa affidarsi alla nostra intuizione per capire il comportamento del nostro programma. In generale per loop semplici non c’è probabilmente bisogno di fermarsi a ragionare sulle lop invariant.

Su un piano più pratico, le loop invariant forniscono:

  1. Una ottima documentazione sia come referenza a noi stessi nel futuro che per spiegare l’obiettivo del ciclo.
  2. Come dimostrazione di correttezza: E’ possibile usarli per scrivere una dimostrazione di correttezza dell’algoritmo – che probabilmente dovrà essere accompagnata da una dimostrazione di terminazione tramite loop variant.
  3. Un ottimo mezzo di ragionamento

Ragionare prima di scrivere è in effetti un’ottima pratica spesso sottovalutata, sull’argomento consiglio la visione di questo talk del premio Turing Leslie Lamport.

Referenze:

Seguendo questi link è possibile consultare anche esempi di utilizzo delle loop invariant per dimostrare la correttezza di alcuni algoritmi.

  • Loop Invariants: Analysis, Classification, and Examples: https://dl.acm.org/doi/pdf/10.1145/2506375
  • Introduction to loop invariants: https://www.cs.scranton.edu/~mccloske/courses/cmps144/invariants_lec_sept2017.html