[Python] inquisitori [was re: Turbopascal??]

[Paolo Bernardi]

On Wed, 2011-01-05 at 18:29 +0100, Giorgio Zoppi wrote:
> Il 05 gennaio 2011 18:03, Daniele Varrazzo <piro a develer.com> ha scritto:
> > On Wed, 5 Jan 2011 17:15:13 +0100, Carlos Catucci
> > <carlos.catucci a gmail.com> wrote:
> >
> >> Il GOTO in C io lo ho sempre considerato una bestemmia.
> >
> > Si vede che non hai mai gestito gli errori. :)
> >
> > Riscrivi una funzione come questa <http://tinyurl.com/2esxn2q> senza usare
> > goto e valuta se il risultato è migliore. Codice limitato a 80 colonne,
> > prego.
> 
> Be facciamo un esempio sul kernel di linux.
> 
> jo a jo-eri:~/Scaricati/linux-2.6.7$ grep -r goto . | wc -l
> 26980
> 
> Penso che nel paper
> http://www.thocp.net/biographies/papers/goto_considered_harmful.htm
> Goto Condiered Harmful, Edsger Dijkstra si riferisse all'abuso di goto.

La critica di EWD al GOTO è conseguenza della sua visione della
programmazione. Dijkstra è stato un accanito sostenitore dei metodi
formali[0][1] come strumento per limitare gli errori nei programmi; in
particolare era solito usare la logica di Floyd-Hoare[2][3].

Se date un'occhiata alla logica di Floyd-Hoare vedrete che prevede
regole per le sequenze di istruzioni, per i loop (while) e per i
condizionali (if), ma NON per i salti come il GOTO. Oltre ai problemi di
leggibilità dati dal suo *abuso*, il suo semplice *uso* rende il
programma in questione indimostrabile coi metodi visti sopra e questo
Dijkstra non lo tollerava. :-)

Paolo

P.S. Dijkstra ha scritto tanta, tanta roba (e molto interessante)...
L'archivio dei suoi documenti (ha anche una bella calligrafia!) è
online:
http://www.cs.utexas.edu/users/EWD/



[0] https://secure.wikimedia.org/wikipedia/en/wiki/Formal_methods

[1] Dijkstra si trova nel bel mezzo della cosidetta "crisi del
software" (vedi la conferenza NATO del '68), ovvero i dispositivi
digitali erano diventati troppo potenti in troppo poco tempo mentre i
programmatori erano ancora legati a tecniche vecchie (suona familiare?)
ed assai foriere di errori. EWD insiste perciò sui metodi formali per
rendere lo sviluppo di programmi meno prono ad errori, ed in particolare
su quelli postulazionali (come la logica di Floyd-Hoare) perché a suo
dire l'oggetto più simile ad un programma è una dimostrazione
matematica, sebbene nonostante la similarità di natura i programmi sono
generalmente molto più complicati di quest'ultime.

[2] https://secure.wikimedia.org/wikipedia/en/wiki/Hoare_logic

[3] ... per la correttezza parziale. Per dimostrare se un programma
termina o meno (cosa che aggiunta alla dimostrazione precedente da la
correttezza "totale") bisogna ricorrere ad altri mezzi ad-hoc, tipo
l'induzione.
-------------- parte successiva --------------
Un allegato non testuale è stato rimosso....
Nome:        signature.asc
Tipo:        application/pgp-signature
Dimensione:  490 bytes
Descrizione: This is a digitally signed message part
URL:         <http://lists.python.it/pipermail/python/attachments/20110105/e2b574c2/attachment.pgp>