Programmeraren som Schaman

Den 4 juni 1996 exploderade den första Ariane 5-raketen, 39 sekunder efter start, på grund av ett programmeringsfel i styrsystemet. Konstruktörerna hade tagit delar av programmen från föregångaren, Ariane 4. Huvudregeln i programmering, att inte ändra i det som fungerar bra, gjorde att de nya förutsättningarna i Ariane 5 inte beaktades (se F&F 1/97). Till en fyrverkerikostnad av 60 miljarder kronor visar detta på ett stort och sedan länge känt problem: det är omöjligt att helt förutsäga beteendet hos komplicerade datorsystem.

Att samma förhållande gäller för hårdvara kan illustreras av t ex incidenten med Intels första Pentiumprocessor. I oktober 1994 upptäcktes att den ibland räknar fel när den dividerar två tal. Kostnaden att ersätta miljontals felaktiga chips uppgick till nära fyra miljarder kronor. Liknande fadäser är legio, om än inte lika synliga, inom alla datorintensiva tillämpningar. Att det gäller för telefonväxlar vet det amerikanskatelefonbolaget AT&T. Den 15 januari 1990 gick halva deras telefonnät ner under nio timmar på grund av ett programfel.

Språk som inte talas

För att beskriva beteenden utgår man dels från viktiga händelser, t ex ”förbindelsen kopplas upp”, ”värdet beräknas”, dels från tillstånd, t ex ”klar att ta emot data”, ”förbindelsen är uppkopplad”. Ett beteende är då möjliga följder av händelser och tillstånd. Det kräver dock viss omsorg att göra beskrivningar som inte kan missförstås.

Om vi tar två viktiga typer av händelser i ett datanät: ”förbindelsen kopplas upp” och ”förbindelsen kopplas ner”, kanske vi vill beskriva att först måste uppkoppling ske, därefter nedkoppling, därefter möjligen uppkoppling följd av nedkoppling osv. Hur ska vi beskriva det helt entydigt? Beskrivningen kanske tycks enkel och klar, men vad är den exakta innebörden av orden ”möjligen” och ”osv”?

Att ge förklaringar av detta slag på svenska (eller något annat naturligt förekommande språk) är hopplöst eftersom varje försök att definiera ett begrepp kräver nya ord som i sin tur ska förklaras. Förklaringarna bottnar aldrig i helt väldefinierade begrepp. Lösningen är att använda s k formella språk. Dessa är inte språk i ordets vanliga mening, eftersom det som kan uttryckas på formella språk är starkt begränsat. Till exempel går det inte att säga ”var snäll och köp lite mjölk på hemvägen”. Begrepp som ”lite” och framför allt ”snäll” är det ingen som har vågat försöka definiera matematiskt. Däremot går det bra med ”uppkoppling och nedkoppling alternerar”. I formella språk är betydelsen av utsagor definierade med matematisk noggrannhet. Man har minskat uttrycksfullheten för att vinna i precision.

Ett exempel på formella språk är s k tillståndsdiagram. I bild kan man beskriva händelserna utan att det blir tvetydigt. Det finns massor av formella språk trots att antalet principer för att beskriva beteenden inte är stort. IT-företagen har helt enkelt ännu inte kunnat enas om en standard. Det är föga troligt att de kommer att göra det inom en snar framtid – inte heller kommer de att enas om att använda ett enda programmeringsspråk.

Skriv först – prova sedan

I datorernas barndom var minnet mycket litet och programmen följaktligen små och få. Programmerarna satte en ära i att hålla hela system i huvudet och rättade programfel, eller dödade löss som man sa, genom att tänka djupt och länge. I dag innehåller den enklaste persondator miljontals programinstruktioner men fortfarande försöker vi avlusa genom intellektuella maratonlopp. Oftast skriver vi dessutom snabbt ihop ett program och försöker kompensera bristen på planering med en grundlig utprovning. Men tidiga flygturer kan lätt sluta i Gripen-gropen.

Funktionsfel kan inte förutsägas, och när de yttrar sig i den lakoniska dödsrosslingen ”system error” blir det ett styvt jobb att spåra orsaken och ett sisyfosarbete att åtgärda den, eftersom varje förändring kan rubba andra delar av systemet. Ingenjören, å sin sida, använder matematiska modeller för att räkna ut viktiga egenskaper hos det som ännu inte är byggt. Om ett kugghjul blir för klent upptäcks detta redan i modellen och man kan ändra konstruktionen. På samma sätt vill en programmerare kunna analysera en modell av ett beteende för att säkerställa att det är acceptabelt. Allra bäst vore det om det fanns en möjlighet att också garantera att modellen är riktig. Här stöter vi dock på patrull. För det mesta saknas metoder som garanterat ger ett korrekt svar. Det finns till och med bevis för att sådana metoder inte kan finnas. Detta visade den brittiske matematikern Alan Turing redan 1936 (se F&F 4/97). Vi kommer aldrig att kunna få allmänna metoder som svarar på frågor som: Uppfyller systemet ett visst krav? Kommer systemet någonsin att slutföra beräkningen? Har två system samma beteende? Är två krav motstridiga?

Listan kan göras lång, och det är lika illa för alla formella språk. Att leta efter allmängiltiga metoder för att svara på sådana frågor är lönlöst. Vi måste hålla till godo med metoder som bara fungerar i vissa speciella fall. Tre vägar har hittills prövats för att komma till rätta med det problemet. Den första innebär att man minskar språkets uttrycksmöjligheter. Om möjligheterna beskärs tillräckligt kraftigt kan frågorna avgöras. Till exempel kan man bestämma en övre gräns för hur stora de tal får vara som datorn kan behandla.

Då går det inte längre att direkt uttala sig om godtyckligt stora tal. En sådan inskränkning kan tyckas harmlös, men har faktiskt stor betydelse i många sammanhang. Ta t ex division av heltal. Skriver man ett program som ska dividera vill man gärna veta att det fungerar för alla heltal, dvs för en oändlig mängd olika tal. I och för sig har varje dator en övre gräns för hur stora tal som kan behandlas, men eftersom dessa gränser är olika för olika datorer är det olyckligt om programmets riktighet är beroende av en sådan inskränkning. Dessutom går det inte att förutsäga vilka uppgifter som kommer att matas in i ett program. Sådana spådomar kommer oftast på skam; därför vill man hellre säkerställa att det fungerar i alla väder. Annars kan det gå som för Ariane 5 där styrdatorn havererade när ett delprogram tog emot ett oväntat och otillåtet stort värde.

Typkontroll hade räddat Ariane

Ett bra exempel på detta är den så kallade typkontroll som finns för många moderna programmeringsspråk. Om det t ex någonstans står att innehållet i en variabel ska ökas med ett, är det rimligt att anta att variabeln måste innehålla ett tal. Om det å andra sidan står att man ska ta första bokstaven i variabeln, bör den innehålla en text. På detta sätt kan man klassificera data i olika typer utifrån sättet som de används på och kontrollera att samma datavärde inte förutsätts ha motstridiga typer på olika ställen av beskrivningen. Haveriet med Ariane 5 skulle ha undvikits om en sådan kontroll hade gjorts av styrprogrammet. En tredje väg består i att acceptera ofullständiga analysmetoder. Det finns metoder där man vet att svaren man får är korrekta, men som inte alltid ger något svar alls. Dessa metoder är inte begränsade av antalet tillstånd.

Dessa ofullständiga metoder är baserade på formell logik, och principen är att hitta bevis i speciella logiska skrivsätt. Om man hittar ett bevis är frågan avgjord. Om inte, kan detta bero antingen på att det inte finns något bevis, eller på att det finns men att man har misslyckats med att hitta det. Det är omöjligt att veta vilket av de två senare alternativen som föreligger.

En fullständig automatisering av sådana metoder är inte att rekommendera med dagens teknologi. När det gäller att leta efter bevis behövs listighet, förmåga att se mönster och allmän erfarenhet. Detta kan man träna ingenjörer till, men det är svårt att programmera datorer att göra det bra. Dessutom är resultatet av en bevisföring ofta mer än det summariska ”utsagan är sann”; man kan i arbetet med att ta fram beviset få en intuitiv insikt om orsakerna. Denna kan vara värdefull i många sammanhang, men är svår att skapa i en dator.

Ett bevis kan kontrolleras

En fullständig bevisföring blir till sin längd jämförbar med den beskrivning som analyseras, eller ofta till och med ännu längre. Det kan lika gärna uppstå ett fel i själva bevisföringen som i programmet som ska kontrolleras. Om sannolikheten att ett misstag begås är proportionell mot längden, är alltså mycket litet vunnet! Skillnaden är dock att ett bevis, men inte ett program, kan kontrolleras på ett mekaniskt sätt. Så även om datorer inte själva kan utföra bevisen kan de i efterhand kontrollera att bevisen är riktiga. Det finns i dag flera program för detta och till och med program som hjälper till litet under arbetet med bevisföringen. Forskningen på området har utvecklats mycket starkt de senaste tio åren och utgör i dag en stor del av datalogisk forskning överhuvudtaget.

Först de senaste åren har resultaten börjat visa sig. I modern systemutveckling vill man ha en begriplig struktur för både form och funktion. Nya språk tvingar programmerarna att ange hur olika programdelar kan kombineras för att undvika att de sätts ihop på fel sätt. Vid säkerhetskritiska tillämpningar i kärnkraftverk krävs en logisk analys som bevisar att beteendet är acceptabelt. Men övergången från kaotisk till välordnad produktion är inte smärtfri. Den inskränker ju friheten för alla våra dataexperter och programmeringsfantomer.