Ny Ph.d-forskning kan gøre programmer beviselige

Lyder lovende, men handler det her om Entscheidungsproblem'et (http://en.wikipedia.org/wiki/Entscheidungsproblem) ?

For hvis det gør, lyder det for godt til at være sandt...

Hvis metoden er forkert - er svaret vel forkert?

Selvom et program, er sandt, kan metoden der anvendes, være forkert.

Der er mange egenskaber, ved programmer, som du kan bevise - i nogle tilfælde, kan du konstruere sprog, som umuliggør "dårlige egenskaber", og du har da til dels løst problemet, ved intet ikke beviseligt lader sig formulere. Eller, at det er relativt simpelt at tjekke, f.eks. ved at søge på en ordre (der er bevisligt ulovligt), eller eksempelvis ved sædvanlig type og syntax tjek.

Hvordan skal vi "bevise" om et program - som et operativsystem - er "korrekt". Måske kan vi end ikke blive enige om, hvordan operativsystem deffineres.

Det vi har chancer for at bevise, er at to forskellige beskrivelser af samme problem er identisk. Dette tror jeg dog også er svært.

Vi har mulighed, for at bevise at programmer - såsom parallel problemer, er deterministiske.

Vi har mulighed for at konstruere programmeringssprog, hvor pointere ikke anvendes på sædvanligvis, og er mere nemt at håndtere beviser for, end i C++ og pascal.

Sådanne sprog, vil måske også øge programmets gennemskuelighed? Måske hænger maskninel analyse og menneskers analyseevne sammen på en måde?

Vi anvender ofte metoder, for at bevise eksempelvis hardware. Reelt, kan vi dog kun bevise det, som vi spørger om. Eksempelvis, kan vi bevise, at vores resultat er deterministisk, og ikke afhænger af skev på forsinkelser, på gates, indenfor det deffinerede. Et sådant "bevis" kræver dog i nogle tilfælde alle muligheder gennemgås.

Igen, findes en omvej til beviset: At konstruere metoder, og programmeringssprog, til at deffinere hardwaren, der ikke tillader designeren at gøre noget, som bevisprogrammet netop ikke vil lade ham gøre. Man går altså den modsatte vej - i stedet for at tillade "ulovligt input", konstrueres et sprog, som umuliggør ulovlige konstruktioner.

Og nu er det pludseligt beviseligt.

Samtidigt, kan vi bevise, at der ikke findes noget beskriveligt problem, der ikke kan indtastes - andet end hvis det vi ønsker at indtaste, ikke er lovligt jfr. det vi ønsker at bevise. Det kan så klares, hvis det absolut skal gøres, ved at analysere hvad vi ønsker, og indlægge "ulovlige ordrer". Nu er det stadigt nemt at bevise - en simpel søgning på ulovlige ordrer, fortæller om vores ting er korrekt. Da vi konstruerer sproget, til at det altid vil gå imod beviset, når en sådan ordre anvendes. Ordren skrædersyes simpelthen til, at umuligt være lovlig. Og det vises, at enhver ulovlighed, kan beskrives udfra denne ulovlighed.

Hvis vi har nogen "egenskaber", som vi ønsker at sikre, vores resultat ikke opnår, er den bedste, og mest sikre metode, at anvende et sprog, som kontrueres til, at denne egenskab umuligt kan programmeres. Er dette ikke nok, til vores normale brug, isolerer vi det farlige, og adderer til sproget. Beviset, er nu en slavisk søgning. Og det er nemt at se, hvem der har begået ulovligheden, hvis de "mærkes" med et fingeraftryk, fra programørene.

Så er det bare retsagen som venter.

D.E. Knuth: ``Beware of bugs in the above code; I have only proved it correct, not tried it.''

(http://www-cs-faculty.stanford.edu/~knuth/faq.html)

Et typisk problem, vi ønsker at kunne bevise, er om et program afslutter - eller går i uendelig løkke.

Først - for at beviset giver mening, må vi kræve, at vores programmeringssprog netop giver mulighed for uendelig løkke, eller rekursion. Antages disse to funktioner for programmeringssproget, at være fjernet, kan det stadigt bruges til bunker af formål, men vi ved, at den umuligt kan gå i løkker, da de ikke findes. Og dermed, er altid et svar, hvis vi venter lang tid nok. Beviset er derfor gjort, på grund af vores programmeringssprogs begrænsninger.

Antages, et "sædvanligt" programmeringssprog, med mulighed for løkker - og ikke mindst uendelige løkker, og uendelig rekursion, samt mulighed for branches osv. så kan vi konstruere et program, der skal løse et problem. I programmet er indprogrammeret et NP problem, med løsningen sandt eller falsk. I tilfælde af sandt, svares ikke, og programmet går i uendelig løkke. Den svarer kun falsk og afslutter så. Kan vi bevise, om programmet afsluttes? Ikke uden, at det er et NP problem. Dog, kan vi analysere den, og sige vi ikke kan garantere for, at den ikke afsluttes. I nogle tilfælde, kan vi bevise programmer - i andre, kan vi ikke. Og det er måske et NP problem, at opdage om programmet afsluttes.

Dette illustrerer måske også idéen i, at udvikle sprog, som ikke har problemet. Dette er et mere sikkert værktøj, der altid fungerer - sammenlignet med en test, der ikke altid kan svare.

Problemet er så kun, hvis sproget "intet kan", eller "ikke kan nok".

Det er ikke altid, at en uendelig løkke, betyder så meget som man umiddelbart tror. Måske analyserer computeren programmet, og arbejder videre med det efterfølgende, hvis det ikke direkte afhænger af resultatet for den uendelige løkke. I princippet kan den uendelige løkke være forkortet bort, fordi at resultatet ikke er brugt. Det interessante er, at når vi lader computeren fortsætte, med det efterfølgende, og køre dette som et andet "task". Vi ved ikke, om vores problem afsluttes, og derfor lader vi computeren kun bruge ledigt tid, som ikke skal bruges på andet, på at løse problemet. Er således andet, kan og vil den fortsætte med dette, meddens problemet sættes nedderst på listen over det som skal bruges tid på. Sædvanligvis, giver dette computeren større svartid. Bruger vi et resultat fra en løkke, fås ikke svar, før computeren har haft tid på at udregne det. Men, det har ikke ødelagt efterfølgende koder, eller sideløbende kode. Måske sletter vi på et tidspunkt skærmen, og er ligeglad med, at feltet ikke er fyldt ud - og så behøver vi ikke at regne det ud. Computeren har måske endog indsét dette, og aldrig udført koden.

Ovenstående er dog ikke et "bevis" for, at uendelige løkker ikke er et problem, fordi at computeren bare fortsætter. Den vil stadigt, anvende resourcer på at løse det umulige. Og derfor, får den væsentligt større forbrug af strøm. Hvor den normalt kunne slappe af, og gå i power down, bruges energien på de umulige opgaver, den stadigt står og kører rundt i. Hastighedsmæssigt, er det dog et mindre problem.

Den måde - som jeg foretrækker - at "bevise" på at et program afslutter, er at kræve hver enkelt programmør opskriver timing specifikationer for deres komponent. Inden for hardware, må du ikke lave en, hvor du ikke angiver timing - både minimum delay, og maksimum delay. Der er simpelthen tekniske data, for hver enkelt komponent. Indenfor software, er analogien store O funktionen. Denne er softwaremandens "timing". Du må ikke lave en funktion, eller blok, uden at angive store O funktioner. Har du store O funktionerne, så du ved alt om, hvilke parametre delays afhænger af i dine moduler, så får du først garanti for at de svarer. Programmøren står inde for det, ved at aflevere store O funktionen.

Vi kan så diskutere, om vi kan bevise den er korrekt. Men problemet, er nu vendt om - fra at programmet skulle stå inde for timingen (store O funktionen), til at skulle bevise den påstulderede funktion, som måske står anført som del af programmeringssproget. Kan et tool undersøge, om påstanden er korrekt, er sproget måske bevist? Atter har vi da et sprog, hvor vi kan føre bevis for at programmet svarer, inden en given tid (komplekstitet). Vi skal måske sætte krav til maksimum kompleksiteten, hvis vi ønsker rimelig svartid. F.eks. en log(n) som maksimum, hvilket svarer til, at vi højst accepterer en "konstant" svartid, og dermed kan sige den svarer indenfor en given tid. Ved n * log(n), skal brugeren gøres opmærksom på dette, ved at procent udregnes, men dette bør undgås, hvis muligt. Brugere hader at vente. Over n * log(n), bør ikke være muligt. Med sådanne krav, kan naturligvis ikke løses alt, men en stor del af software programmer kan løses.

Hvis vi ønsker at bevise noget, må vi vide hvad vi går efter. I nogle tilfælde, kan konstrueres sprog, der gør, at vi er sikker på, at ethvert input, altid overholder vore krav. Hvis et sådant sprog, er nok til at beskrive vore problemer, er det måske det bedste at bruge, for så ved vi, at ingen begår ulovlighed. I tilfælde som "determinisme", kan vi i princippet have sprog, hvor alt som sædvanlige programmer kan gøre er muligt, og hvor vi står inde for determinismen. Dog, er ikke muligt med random. I tilfældet, at garentere, at der er en svartid - da vil et begrænset sprog, ofte give problem.

Det bedste - syntes jeg - er at alle programmører skal stå inde for programmets svartid, og lagerforbrug, og at disse ting dokumenteres i programmer og rutiners tekniske datablade. Bruges en C ordre, kan vi slå op i manualen, og se dens store O funktion. Den står måske også angivet i koden, hvis vi har source.

I mange sammenhænge - hvor brugere og hvemsomhelst skal have adgang til kodning, kan være en fordel at begrænse sproget, således det ikke tillades løkker og rekursion, såfremt dette er nok for brugeren, og de programmører der skal "konfigurere".