Newsgroup: it.scienza.informatica
Titolo: Indecidibiltà e ingegneria del software (era: Re: Programmazione 'artigianale')

 >>
questa non era una risposta alla mia affermazione, perché io non ho detto
che i programmi che girano sui calcolatori reali terminano sempre. Stai
forse facendo confusione tra il dire che il problema della fermata è
decidibile e il dire che tutti gli algoritmi terminano sempre?
6) Sulla questione "problema di decisione" vs "caso di decisione": tu
giustamente dici che che se un problema è indecidibile questo non significa
che sia impossibile trovare la soluzione di quel problema su una
particolare istanza; quello che sembri ignorare però è che non è nemmeno
detto che sia impossibile trovare un insieme di istanze su cui il problema
diventa decidibile! Anzi questo è quello che avviene normalmente: quando si
scopre un problema indecidibile, i teorici vanno a caccia di sottoinsiemi
decidibili, e non è affatto detto che questi sottoinsiemi non siano
talmente ampi da contenere tutti i casi che interessano nella pratica,
tant' evvero che, come avevo già detto, di solito la difficoltà non è data
dall' indecidibilità ma dalla complessità computazionale (che anch' essa
dipende dall' insieme di casi che si prendono in considerazione)
Conclusione:
L' ingegneria del software è sicuramente una disciplina che deve fare
ancora molta strada, ma le sue difficoltà dipendono da tutto meno che dal
fatto che esistono problemi indecidibili; perché, prima di tutto,  per
quello che ho detto nel punto 4), questi non esistono nella pratica; ma
anche se esistessero non si dovrebbe far altro che cercare di inquadrare i
casi che interessanno all' interno di un sottoinsieme decidibile e siccome
questo sottoinsieme esiste sempre in pratica, in realtà la difficoltà stà
nel trovare un sottoinsieme che abbia una complessità computazionale
accettabile. Ancora più concretamente tutte le difficoltà dell' ingegneria
del software stanno nel riuscire a trovare un formalismo per scrivere i
programmi  che, da una parte, consenta di risolvere i problemi di verifica
della correttezza e di rispondenza a determinati requisiti, e dall' altra,
non che non limiti troppo la classe dei programmi scrivibili con esso
(perché da qualsiasi punto di vista teorico li si guardino, i programmi
reali sono tutti "semplici"), ma che sia realmente accettato e usato in
pratica dai programmatori. E' in quest' ultimo problema che i cosiddetti
metodi formali hanno fallito.
Un' ultima osservazione sul paragone con gli ingegneri edili quando si dice
che questi hanno tutte le leggi della fisica a disposizione per verificare
i loro progetti. In realtà le leggi della fisica non hanno lo stesso grado
di certezza delle verità matematiche, ossia non si può dire con lo stesso
grado di certezza che una legge fisica varrà sempre e comunque in ogni
situazione possibile; ma di questo gli ingegneri edili se ne infischiano
allegramente: gli basta sapere che nei casi concreti in cui si troverà ad
applicarle, quelle leggi sono state verificate con grande precisione. A ben
vedere quindi la situazione non è diversa da quella dell' ingegnere
informatico che, in certi casi, sa che non potrà scrivere un algoritmo
capace di risolvere tutti i casi teoricamente immaginabili, ma ciò non gli
impedisce di cercare algoritmi per risolvere solo il sottoinsieme di
problemi che gli interessano nella pratica ( l' unica differenza ovviamente
è che gli informatici teorici non hanno ancora fornito agli ingegneri
questi algoritmi, cosa che i fisici hanno già fatto per gli ingegneri
edili...)
Thomas B.
P.S. Io non mi offendo mai, ma prima di dire che queste discussioni ti
ricordano quelle di un paziente psicotico o che vado in giro a dire falsità
non sarebbe meglio riflettere un po'? In fondo quando uno fa affermazioni
che sembrano totalmente sbagliate c'é anche il caso che in realtà non
stiamo capendo affatto quello che sta dicendo :-)
P.P.S C'é una sola cosa che ha mi "offeso" e che mi fa prudere le mani
dalla voglia di replicare, per cui replico ora (in tono scherzoso, eh!) :
rileggitelo tu un buon libro di teoria della calcolabilità! ;-)
Ciao

 edili...)
Mi correggo il Non plus ultra e' questa tua ultima perla
Ti ripeto che assunta vera la tesi di Church--Turing,
questi algoritmi che tu ti aspetti ti vengano forniti
dagli informati teorici NON esistono e lo sappiamo gia' da ora.
Questa era la speranza degli uomini di inzio 1900
che speravano di ``meccanizzare'' la dim. matematica
(et simili) [il progetto di Hilbert ti dice nulla?]
poi e' venuto G\"odel Turing.......
Attualmente la ricerca si e' indirizzata
verso la QC per studiare la possibilita' di superare
il limite del T-calcolabile.
[Q.C. sta per Quantum Computation]
--
Saluti,
 
cibe...@libero.it
Studia MENO
Studia MEGLIO

 Studia MEGLIO
E' il consiglio che do a te! Guarda che le cose che ti sto dicendo sono
*veramente* ovvie e banali, al punto che se uno si appassiona troppo ai
problemi teorici rischia di dimenticarsene. Sei tu che hai tirato fuori
funzioni ricorsive primitive, goedelizzazioni, Quantum computer (!) quando
a me basta molto meno, per dimostrare quello che dico...
Ciao.

decisione, su queste mdt modificate, sono decidibili.
OK. Imponendo la terminazione dei cicli dopo un certo numero di
iterazioni e limitando la memoria allocabile si ottengono certamente
dei programmi decidibili: tuttavia cio' in un certo senso "falsa" il
programma originale (senza limitazioni). Infatti non si ha la garanzia
che i limiti imposti siano coerenti col risultato che ci si aspetta
dal programma originale. In questo senso la correttezza di un generico
programma non e' testabile in modo meccanico.
Comunque riguardo alla questione dell'ingegnerizzabilita' del software
sono d'accordo al 100% con te. Negarne la possibilita' (con le
argomentazioni di ciberneta) e' come dire che non puo' esistere
l'ingegneria edile perche' il principio di indeterminazione di
Heisenberg impedisce la misura esatta della lunghezza di una trave. 
E' ovvio che nessun ingegnere si aspetta una bacchetta magica che gli
risolve indiscriminatamente tutti i problemi, ma cerca di usare
strumenti (anche disparati e disomogenei) che possano aiutarlo per
quanto possibile: per quanto riguarda il testing di validita' dei
programmi esistono diversi metodi, assai piu' "teorici" e
"scientifici" che artigianali (Floyd, Manna, etc). Naturalmente non
c'e' la "bacchetta magica", ma non per questo e' il caso di negare
tout cort la possibilita' di ingegnerizzare il software. Ciao

 Heisenberg impedisce la misura esatta della lunghezza di una trave.
E/o la sua posizione, cosa ancora più preoccupante :-)))
--
Alessandro Monti


Bah....
Per ``dimostrare'' quello che dici basterebbe che l' aritmetica di Peano
fosse contradditoria.....
:-)
(Lo sai che la non contradditorieta' di un sistema formale e' dimostrabile
solo all' interno di sistemi formali contradditori?
Un nuovo shock?
Spero di no!)
--
Saluti,
 
cibe...@libero.it
--
_________________________________
Mensch ist Automat !
Kybernetik uber alles !!!
_________________________________
--
__________________
Have a lot of (de)fun
__________________

 tout cort la possibilita' di ingegnerizzare il software. Ciao
Esattamente, esistono decine di libre che parlano di questi argomenti,
evidentemente ciberneta non li conosce o li considera scritti da imbecilli.
Ovviamente bisogna ammettere che questi metodi sono da considerare
fallimentari, perché nessuno ha praticamente ottenuto una larga
applicazione a livello industriale ( e purtroppo continuiamo ad avere
programmi pieni di bug) ma questo dipende da tutto meno che dall'
indecidibilità.

 Ti basta? O e' poco serio?)
Per articoli seri intendevo quelli fatti con definizioni e teoremi. Non so
tu quanti ne hai letti fatti in questa maniera, ma in tutti quelli che ho
letto io, i sistemi formali di calcolo quantistico che venivano definiti,
non estendevano nel modo più assoluto l' insieme delle funzioni
calcolabili.
Gli altri per ora sono solo speculazioni, magari molto interessanti, ma
sempre speculazioni.
Ora ti dovrei anche spiegare perché ritengo estremamente implausibile che
si possa estendere l' insieme delle funzioni calcolabili, ma preferirei
rimandare la cosa ad un momento in cui tu mi sembrerai più ben disposto a
ricevere spiegazioni. (Comunque, per darti qualche indizio: la definizione
delle funzioni calcolabili si basa sostanzialmente su poche semplici
condizioni, non appena violate le quali, è facile dimostrare che tutte le
funzioni diventano calcolabili, il che ovviamente non è la soluzione del
problema. Appare quindi molto difficile trovare una via di mezzo. E ti
ripeto ancora che chi si occupa veramente di Quantum Computation è
impegnato soprattutto a cercare di risolvere, oltre ai problemi di fisica
realizzabilità, i problemi NP in tempo polinomiale, e su questo argomento
mi piacerebbe sapere qualcosa di più perché non sono riuscito a capire bene
cosa è stato dimostrato in questo campo).
A risentirci.
Thomas

indecidibilità.
Sempre d'accordo al 100%. Anche a me le questioni di informatica
teorica sembrano lontanissime dalle reali problematiche attuali del
software. Comunque volevo intendere che un risultato teorico negativo
(problema della fermata) non deve giustificare un disfattismo
generalizzato verso ogni altro aspetto teorico. Ciao

Un nuovo shock?
Questa affermazione, piu' che shockante, e' semplicemente falsa. Ciao

generalizzato verso ogni altro aspetto teorico. Ciao
Questo e' verissimo. Del resto sarebbe come rinunciare alla ricerca in logica 
perche' c'e' il teorema di Godel.
-- 
God is Real, unless declared Integer.
ObjectZone - 
http://space.tin.it/computer/csadun

ottieni solo occhiate stralunate.
E vabbe', questo e' piu' che comprensibile.
A meno che non devi progettare il sistema di controllo dello shuttle, nel
qual caso ci si aspetta che il committente sappia il fatto suo, e' difficile
che l'azienduccia che vuole il programmino di fatturazione conosca il Lotos
o la semantica denotazionale.
Se lo conoscesse molto probabilmente saprebbe anche buttare giu' due righe
di progetto e magari ti assume non come progettista ma come manovale.
Marco

di progetto e magari ti assume non come progettista ma come manovale.
Comprensibile, e' comprensibile. Come e' comprensibile che il docente medio non 
sia punto interessato al Kernighan&Ritchie. Viene pagato lo stesso, no?
Il problema e' che non succede solo con le azienducce che fanno sistemucci, 
anzi.
E queste non-azienducce fanno sistemi che devono partecipare in interazioni 
complesse. Specificare queste interazioni richiede competenza in informatica 
teorica (per sapere cosa si puo' e non si puo' fare) e  linguaggi di 
comunicazione appropriati (per descrivere e comunicare il come si vuol fare 
quello che si puo' fare :). 
Quando questi requisiti sono ignorati, su progetti non banali, i risultati sono 
i soliti: ritardi, budget alle stelle, fallimenti o abbandoni di progetto.
La cosa buffa e' che tali strumenti non sono, per lo meno nella forma 
"pratica", ne' particolarmente astrusi ne' particolarmente esotici: molti sono 
in giro da decenni, e se uno ha un minimo di familiarita' con la matematica (e 
da uno che costrusce software, io me la aspetterei ;-) si imparano e si usano 
con facilita' - almeno la stessa facilita' con cui si impara ad usare l'ultima 
versione di visual basic o l'estensione java della settimana.
Ma - essendo considerati "teoria" - sono semplicemente rifiutati a priori. Un 
po' come lo stereotipo di studente di letteratura che, di fronte a qualunque 
cosa odori minimamente di matematica, si ritrae ululando :) senza nemmeno 
considerare la possibilita' di avvicinarcisi.
Il perche' e il percome di questo ha probabilmente origini lontane e complesse, 
che vanno dalla struttura della scuola superiore al modo in cui gli 
insegnamenti sono portati avanti nelle universita', ad una generale giovinezza 
ed immaturita' del mondo informatico commerciale. Ma e' un discorso lungo. :)
-- 
God is Real, unless declared Integer.
ObjectZone - 
http://space.tin.it/computer/csadun/