Verifica di correttezza
Il mio corso di Introduzione alla Programmazione consiste praticamente nel fare solo verifiche di correttezza di vari algoritmi (semplici). Una volta imparato il meccanismo, trovo veramente inutile insistere su questo argomento. E' principalmente una perdita di tempo, per quanto mi riguarda, perché per programmare bene non serve fare queste verifiche per ogni algoritmo.
Dalla vostra esperienza, da Programmazione I in poi le cose cambiano?
Dalla vostra esperienza, da Programmazione I in poi le cose cambiano?
Risposte
Dipende da cosa intendi per "Programmazione I"...
Che corso di laurea frequenti? Informatica?
Che corso di laurea frequenti? Informatica?
Yep. Arriveremo fino a Programmazione III. Ho visto gli argomenti di quest'ultimo corso e non lo trovo impegnativo.
Personalmente (premetto che frequento ingegneria informatica) non ho mai fatto verifica alcuna di algoritmi e roba simile.
Gli esami di programmazione della triennale sono solo due. Siamo partiti direttamente con l'esame Elementi di Informatica che consisteva nelle basi del C++: variabili, funzioni, vettori, puntatori sostanzialmente. Poi c'era Programmazione I che era il continuo, ovvero si trattavano le classi e l'astrazione dei dati, ereditarietà, polimorfismo, allocazione dinamica della memoria. E poi stop... niente più esami di programmazione fino alla specialistica dove ci sarà Programmazione II che riguarda il linguaggio java. Sicuramente molto poco rispetto alla programmazione che si insegna nei corsi di laurea di Informatica... ecco perché ti chiedevo cosa frequentassi, magari il "Programmazione I" tuo è diverso da quello che ho dato io. In ogni caso concordo sul fatto che una persona abituata a ragionare possa trovare inutili certi esercizi di base sugli algoritmi e vorrebbe passare direttamente alla parte pratica... il mio professore insisteva nel dire che un programma andava sempre scritto prima su carta e verificato a mano, mentre la scrittura del codice sarebbe dovuto essere l'ultimo passo. Non ho mai seguito quella procedura però...
Gli esami di programmazione della triennale sono solo due. Siamo partiti direttamente con l'esame Elementi di Informatica che consisteva nelle basi del C++: variabili, funzioni, vettori, puntatori sostanzialmente. Poi c'era Programmazione I che era il continuo, ovvero si trattavano le classi e l'astrazione dei dati, ereditarietà, polimorfismo, allocazione dinamica della memoria. E poi stop... niente più esami di programmazione fino alla specialistica dove ci sarà Programmazione II che riguarda il linguaggio java. Sicuramente molto poco rispetto alla programmazione che si insegna nei corsi di laurea di Informatica... ecco perché ti chiedevo cosa frequentassi, magari il "Programmazione I" tuo è diverso da quello che ho dato io. In ogni caso concordo sul fatto che una persona abituata a ragionare possa trovare inutili certi esercizi di base sugli algoritmi e vorrebbe passare direttamente alla parte pratica... il mio professore insisteva nel dire che un programma andava sempre scritto prima su carta e verificato a mano, mentre la scrittura del codice sarebbe dovuto essere l'ultimo passo. Non ho mai seguito quella procedura però...
Nessuno segue quella procedura, secondo me 
. Un mio amico di ingegneria informatica, sempre qui a Padova, ha fatto come te: direttamente esercizi di programmazione (in Java, però). D'accordo che a Informatica si fa più teoria, ma passare un'ora e mezza a provare le correttezza di due algoritmi mi sembra esagerato..
. Un mio amico di ingegneria informatica, sempre qui a Padova, ha fatto come te: direttamente esercizi di programmazione (in Java, però). D'accordo che a Informatica si fa più teoria, ma passare un'ora e mezza a provare le correttezza di due algoritmi mi sembra esagerato..
No Crook, è molto importante.
Quando hai scritto un algoritmo, che magari nella tua mente è chiaro, ma poi non funziona, è importante riuscire a capire dove sia l'errore.
Molte volte prende più tempo che non scrivere l'algoritmo stesso.
Quando hai scritto un algoritmo, che magari nella tua mente è chiaro, ma poi non funziona, è importante riuscire a capire dove sia l'errore.
Molte volte prende più tempo che non scrivere l'algoritmo stesso.
Sì, può essere utile, sono d'accordo, ma raramente (per quanto mi riguarda). Ma le verifiche di correttezza che ci fanno fare non fanno altro che ribadire quello che dice già l'algoritmo. Gli errori che puoi trovare con le verifiche si possono trovare più velocemente con un debug accurato..
In teoria Cheguevilla ha ragione... per algoritmi difficili a volte è indispensabile un controllo preventivo, altrimenti si rischia di scrivere una mole di codice a vuoto. Tuttavia data l'enorme semplicità dei programmi che assegnano nei corsi universitari, in questi casi chi ha un po' di dimestichezza con la programmazione può benissimo passare direttamente alla stesura del codice.
"Crook":
Sì, può essere utile, sono d'accordo, ma raramente (per quanto mi riguarda). Ma le verifiche di correttezza che ci fanno fare non fanno altro che ribadire quello che dice già l'algoritmo. Gli errori che puoi trovare con le verifiche si possono trovare più velocemente con un debug accurato..
ma è una verifica della "logica" dell'algoritmo o della sintassi del programma? facci un piccolo esempio.
nel primo caso potrebbe essere un esercizio di grandissima utilità, giacchè implica un passo che spesso viene saltato a piè pari (in ogni materia, non solo in informatica):
"capire il problema"
tony
per quanto noioso possa essere verificare un algoritmo al primo anno (io l'anno scorso l'ho odiato...), ho scoperto che in generale esiste un vero e proprio filone di ricerca nella verifica formale e matematica dei programmi. La cosa non e' per niente banale ed e' utilizzata anche nella realta' per applicazioni di software che deve __assolutamente__ essere corretto e sicuro.
La verifica formale e matematica dei programmi e' una delle tante applicazioni della logica matematica nell'informatica. (Questa cosa e' divertente perche' di fatto l'informatica e' nata come un'applicazione della logica)
La verifica formale e matematica dei programmi e' una delle tante applicazioni della logica matematica nell'informatica. (Questa cosa e' divertente perche' di fatto l'informatica e' nata come un'applicazione della logica)
"tony":
facci un piccolo esempio.
Ecco un ciclo while, con le asserzioni di correttezza.
/* P: 0 <= n <= 100, P[0..n-1] = PP[0..n-1] */
j = 0;
/* R:
0 <= j <= n-j <= n <= 100, P[j..n-j-1] == PP[j..n-j-1],
P[i] == PP[n-i-1] per ogni i == 0..j-1 e per ogni
i == n-j..n-1 */
while (j < n-j-1) {
/* P1 uguale R && j < n-j-1:
0 <= j < n-j-1 < n-j <= n <= 100, P[j..n-j-1] = PP[j..n-j-1],
P[i] == PP[n-i-1] per ogni i == 0..j-1 e per ogni
i == n-j..n-1 */
/* P2 uguale P1 con evidenziate P[j] e P[n-j-1]:
0 <= j < n-j-1 < n-j <= n <= 100,
P[j+1..n-j-2] = PP[j+1..n-j-2], P[j] = PP[j],
P[n-j-1] = PP[n-j-1],
P[i] == PP[n-i-1] per ogni i == 0..j-1 e per ogni
i == n-j..n-1 */
t = P[j]; P[j] = P[n-j-1]; P[n-j-1] = t;
/* P3 uguale P4 con evidenziate P[j] e P[n-j-1]:
0 <= j < n-j-1 < n-j <= n <= 100,
P[j+1..n-j-2] = PP[j+1..n-j-2],
P[j] = PP[n-j-1], P[n-j-1] = PP[j],
P[i] == PP[n-i-1] per ogni i == 0..j-1 e per ogni
i == n-j..n-1 */
/* Provare che P3 implica P4 */
/* P4 uguale R(j<--j+1):
0 <= j+1 <= n-j-1 <= n <= 100,
P[j+1..n-j-1] == PP[j+1..n-j-1],
P[i] == PP[n-i-1] per ogni i == 0..j e per ogni
i == n-j-1..n-1 */
j++;
/* R */
}
/* P5 uguale R && j >= n-j-1:
0 <= n-j-1 <= j <= n-j <= n <= 100,
P[j..n-j-1] == PP[j..n-j-1],
P[i] == PP[n-i-1] per ogni i == 0..j-1 e per ogni
i == n-j..n-1 */
/* Provare che P5 implica Q */
/* Q: 0 <= n <= 100, P[i] == PP[n-i-1] per ogni i == 0..n-1 */
Provate a contare le righe di codice effettive...
E' palese che al primo anno non possano farti esaminare il codice per il quale veramente ti serviranno le verifiche di correttezza... ergo sorbiscitele 
tutta salute informatica...
tutta salute informatica...
grazie dell'esempio, Crook
mamma mia che roba!
quei quattro statement invertono l'ordine degli elementi dell'array, e va bene
ma le asserzioni di correttezza contenute nei commenti, come vanno interpretate?
(non avevo mai visto un simile linguaggio)
dai, fatto 30, fai 31 e spiegamene una!
grazie
tony
mamma mia che roba!
"Crook":
... Provate a contare le righe di codice effettive...
quei quattro statement invertono l'ordine degli elementi dell'array, e va bene
ma le asserzioni di correttezza contenute nei commenti, come vanno interpretate?
(non avevo mai visto un simile linguaggio)
dai, fatto 30, fai 31 e spiegamene una!
grazie
tony
La prima asserzione P è la precondizione, R è l'invariante del ciclo e Q è la postcondizione. Le asserzioni tra le righe di codice rappresentano lo stato del ciclo in quel punto. Ad esempio se si chiama con $P_1$ la prima asserzione del ciclo, con $P_2$ la seconda etc, deve essere vero che $P_1=>(P_2)_(S)$, dove $S$ è l'espressione tra $P_1$ e $P_2$.
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo