Sintesi e sfide: controllo del flusso

Ciò che l’unità ha ottenuto

L’unità si era proposta di insegnare a governare l’ordine di esecuzione con decisioni e cicli, e a ragionare sulla loro correttezza: che ogni caso venga trattato, che ogni ciclo faccia ciò che deve e che termini. Lo scopo è stato raggiunto appoggiandosi solo su ciò che l’introduzione ha dichiarato di dare per scontato: le condizioni dell’unità 3, i tipi dell’unità 2, e la traccia e la variante della lezione 1.1. Il programma che calcolava il massimo comune divisore con tre passi fissi, e che, a seconda dei dati, rispondeva male o divideva per zero, è stato sostituito da un ciclo di tre righe, e ora si può dimostrare che quel ciclo è corretto per tutti i dati non negativi.

Decisioni

La lezione Decisioni ha insegnato l’istruzione if, sempre con le graffe. Ha mostrato che in una catena di else if si esegue il primo ramo la cui condizione è vera, in modo che il caso reale di ciascun ramo è la sua condizione insieme alla negazione di tutte le precedenti; di qui l’importanza dell’ordine, e il fatto che un ramo possa restare irraggiungibile senza avviso. Ha stabilito il criterio di correttezza di ogni decisione: i suoi casi devono essere disgiunti (lo sono per la forma della catena) ed esaustivi (lo sono se termina con else), e devono coincidere con quelli della specifica, il che si testa all’interno di ciascun caso e da ciascun lato di ciascun bordo. Ha presentato l’operatore condizionale, per scegliere tra due valori brevi senza una decisione intera. Si è chiusa con enum class e switch, del quale il compilatore segnala il caso dimenticato.

Cicli

La lezione Cicli ha presentato while, do e for come tre forme di uno stesso meccanismo: il while valuta la sua condizione prima di ogni iterazione e può non farne nessuna; il do ne fa almeno una; il for riunisce nella sua intestazione l’inizializzazione, la condizione e l’aggiornamento, e la sua variabile di controllo vive solo nel ciclo. Ha insegnato le loro equivalenze, la tabella di traccia, con $k + 1$ valutazioni della condizione per $k$ iterazioni di un while che termina per la sua condizione (e $k$ valutazioni in un do), e il conteggio delle iterazioni dall’intestazione, che previene l’errore di uno. Ha aggiunto break, continue e i cicli annidati, il cui corpo interno si esegue un numero di volte dato da una somma: $m \cdot p$ con limiti fissi, $n(n + 1)/2$ con il triangolo.

Progettare cicli corretti

La lezione Progettare cicli corretti ha fatto del ciclo un oggetto di progettazione. Ha riunito gli schemi (contatore, accumulatore, massimo e minimo, sentinella e flag), ciascuno definito da ciò che la sua variabile significa dopo ogni iterazione. Ha definito l’invariante, un’affermazione che vale ogni volta che si valuta la condizione, con i suoi tre obblighi: inizializzazione, conservazione e conclusione, che insieme alla condizione falsa dà la postcondizione; e lo ha riconosciuto come un’induzione sul numero di iterazioni. Ha insegnato a progettare a ritroso, dalla postcondizione all’invariante e dall’invariante al corpo. Ha giustificato la terminazione con la variante, e ha mostrato tre cicli in cui l’aritmetica di C++ la invalida: quello su numeri reali che salta 1.0, il contatore senza segno che ricomincia dall’altro estremo e il contatore con segno che va in overflow. Ha dato, infine, il primo contatto con il debugger.

Algoritmi numerici

La lezione Algoritmi numerici ha applicato quanto precede a quattro algoritmi classici, scritti dentro main e dimostrati. La primalità per divisioni di prova, con la proposizione secondo cui basta arrivare a $\sqrt{n}$ e con la condizione d <= n / d, che non va in overflow dove d * d <= n ci va. L’algoritmo di Euclide, con l’invariante $\operatorname{MCD}(a, b) = \operatorname{MCD}(a_0, b_0)$ e la variante $b$, e i suoi due pericoli in C++: il risultato negativo e la divisione per zero se la condizione si valuta dopo il corpo. Il cambio di base per divisioni successive e lo schema di Horner, che valuta un polinomio con una moltiplicazione per coefficiente. E la bisezione, garantita dal teorema dei valori intermedi e governata da un contatore intero il cui numero di iterazioni si calcola in anticipo.