[tc] [OT]Re: lettera alla commissione europea

[Davide Prina]

167_ wrote:

> Il giorno mar, 31/10/2006 alle 23.42 +0100, Luca Brivio ha scritto:
>> Il giorno Tue, 31 Oct 2006 19:06:35 +0100
>> Davide Prina ha scritto:
>>
>>>> a) nessuno leggendo un programma può essere sicuro che non contiene
>>>> errori o codici malevoli. Ci sono molti risultati formali della
>>>> logica-matematica che hanno dimostrato questo.
>>> veramente è stato dimostrato che non è possibile dimostrare la 
>>> correttezza formale di un algoritmo, se non ricordo male si dice che
>>> è un problema NP-completo.
>> Se è un problema NP-completo per definizione ha una soluzione. Il che
>> non esclude che essa possa essere impraticabile sopra una certa
>> complessità dell'algoritmo.
>>
>> Tutto questo non so che cosa abbia a che fare con i bug...

se non puoi dimostrare che una cosa è corretta, allora non puoi 
dimostrare che è priva di bug

> in realta ci sono due grossi risultati che mettono in luce
> l'inadeguatezzza della logica e dunque  la impossibilità di verifcare
> formalmente in maniera automatica che un programma abbia una certa
> semantica  (operazionale o denotazionale che sia ):
> 1) il teorema di incompletezza di godel
> 2) (derivabile dal punto 1 )il fatto che non esiste un algoritmo che ti
> dice se un programma termine (tale problema e' in realta semidecidibile:
> l'algortimo migliore ti puo rispondere SI o puo' bloccarsi senza fornire
> risposta .) 

accidenti la mia memoria inizia a perdere i colpi.
Mi ricordavo che era impossibile dimostrare la correttezza formale di un 
algoritmo ... però non mi ricordo quasi più nulla detta teoria che ci 
sta sotto

Ciao
Davide

-- 
Dizionari: http://linguistico.sourceforge.net/wiki
Strumenti per l'ufficio: http://it.openoffice.org
GNU/Linux User: 302090: http://counter.li.org
Non autorizzo la memorizzazione del mio indirizzo su outlook