Hur verifieras programkomponenter och bibliotek?

I stället för att försöka verifiera hela system koncentreras insatserna ofta på att modellera och verifiera individuella kritiska programkomponenter. I modern objektorienterad programmering representeras dessa komponenter huvudsakligen av "klasser" som kapslar in både data och de metoder som arbetar på dessa data. För olika objektorienterade programmeringsspråk har "beteendeinterface-specifikationsspråk" utvecklats, som beskriver inte bara de syntaktiska gränssnitten för klasser, utan även deras semantiska beteende genom logiska förutsättningar och postvillkor för deras metoder samt logiska invarianta för deras objekt. Grundprinciperna för korrekthet i metoder och procedurer behandlas i kapitel 8. För att specificera det externa beteendet hos klasser utan att exponera deras interna representation är det ofta nödvändigt att relatera dessa klasser till "modeller" (exempel på sådana modeller är axiomatiskt specificerade abstrakta datatyper som diskuteras i kapitel 6).

År 2015 visade ett försök att använda KeY för att verifiera sorteringsalgoritmen i Java-biblioteket (en hybridkombination av merge sort och insertion sort, kallad "Timsort") att denna allmänt använda Java-metod faktiskt innehöll en bugg; en korrigerad version kunde framgångsrikt verifieras. År 2017 visades korrektheten för en annan sorteringsalgoritm tillgänglig i Java-biblioteket, "Dual Pivot Quicksort". År 2018 användes KeY för att verifiera korrektheten hos Hyperledger Fabric Chaincode, ett protokoll för smarta kontrakt baserat på blockkedjeteknik. 2020 specificerades och verifierades kärnkomponenter av EVA (det Java-baserade stödsystemet för val i kommuner och län i Norge) formellt i JML och verifierades med KeY.

En annan viktig aspekt av verifiering handlar om verifierade kompilatorer. Verifieringen av datorprogram baseras vanligtvis på en logisk modell av det högnivåspråk i vilket källkoden är skriven. Eftersom denna källkod inte är körbar i sig själv, kompileras den vanligtvis till en faktiskt körbar form, ett program i maskinspråket för den underliggande datorprocessorn. Denna översättningsprocess i sig utgör en potentiell källa till fel, dvs. den genererade maskinkoden kan bete sig annorlunda än förväntat utifrån den logiska analysen av den ursprungliga källkoden. Därför är det en värdefull målsättning att verifiera själva kompilatorn. Problematiseringen av kompilatorverifiering har hanterats av "CompCert"-projektet som startades 2007 av den franske datavetaren Xavier Leroy. Dess huvudsakliga resultat är en verifierad kompilator för en stor delmängd av C99-programmeringsspråket, som genererar effektiv kod för PowerPC, ARM, RISC-V, x86 och x86-64-processorer. Kompilatorn är skriven i specifikationsspråket för bevisassistenten Coq i en rent funktionell stil, och från denna Coq-specifikation genereras körbar kod i det funktionella språket Caml.

Från 2015 har CompCert-kompilatorn varit kommersiellt tillgänglig. År 2017 användes den för att certifiera en mycket säkerhetskritisk industriapplikation, en digital motorenhet som styr reservdieselaggregat för kärnkraftverk, enligt IEC 60880-standarden för kontrollsystem i kärnkraftverk. Trots att CompCert fortfarande förlitar sig på en icke verifierad implementation av Caml, har "CakeML"-projektet, som startades 2012, skapat en verifierad kompilator som själv är skriven i det språk den verifierar, en delmängd av Standard ML. Denna kompilator kan kompilera sig själv och därmed skapa ett verifierat körbart program som bevisligen implementerar kompilatorn själv.

Hur logik kan förbättra programmering och formella metoder: En inblick i teoretiska grunder och praktiska tillämpningar

I den här boken undersöker vi logikens betydelse för att förstå och förbättra programmering, särskilt när det gäller formella metoder och formell semantik. Den metodiska tillämpningen av logik har blivit ett viktigt verktyg i utvecklingen av programvara och system, särskilt i industriella miljöer där säkerhet och korrekthet är avgörande. För att kunna förstå de praktiska tillämpningarna krävs en grundlig förståelse av de teoretiska ramverk som ligger till grund för dessa metoder.

Boken har en bred målgrupp, från studenter och yrkesverksamma inom datavetenskap och datamatematik till de som är intresserade av att förstå den logiska strukturen i programmering. Eftersom vi vill ge en så självständig presentation som möjligt utan att förutsätta förkunskaper inom logik eller matematik, presenterar vi de grundläggande idéerna om logik och matematik som behövs för att arbeta med formella metoder. Samtidigt försöker vi hålla fokus på den "logiska" perspektiven på dessa områden, vilket skiljer sig från många andra framställningar av dessa ämnen.

Kapitel ett, "Syntax och Semantik", introducerar grundläggande begrepp som är avgörande för förståelsen av bokens huvudteman. Här behandlas kontextfria grammatiksystem, som är de induktiva definitionerna av formella språk representerade av abstrakta syntaxträd. Typ- och logiska inferenssystem begränsar dessa språk till vissa "välformade" uttryck, och semantiska funktioner definieras för att ge mening åt dessa uttryck genom att koppla dem till matematiska objekt. I detta sammanhang är induktion, särskilt strukturell induktion, ett kraftfullt verktyg för att resonera om dessa konstruktioner.

Vidare utvecklas de här begreppen i följande kapitel. I kapitel två introduceras syntax och semantik för första ordningens logik, vilket utgör kärnan i boken. Kapitel tre går djupare i resonemanget om logisk bevisföring och introducerar en variant av sekventiell kalkyl som en formell ram för att konstruera bevis. I kapitel fyra behandlas byggandet av modeller, där vi undersöker hur vi med hjälp av logikens språk kan konstruera modeller av verkligheten – teorier och datatyper som vi sedan arbetar med.

Begreppet rekursion, som behandlas i kapitel fem, är avgörande för att förstå semantiken för olika former av rekursion, inklusive induktiva och koinduktiva definitioner av funktioner och relationer. Här tillämpas en restriktiv variant av fixpunktsteori för att behandla dessa komplexa begrepp.

I kapitel sju diskuteras de formella semantiska teorierna för programmeringsspråk, där vi tillämpar de tidigare introducerade typ- och logikmodellerna på att beskriva kommandobaserade programmeringsspråk. Vi behandlar både denotationell och operationell semantik för att modellera program och deras körning. Denotationell semantik kopplar programkommandon till delvis funktioner på programtillstånd, medan operationell semantik betraktar kommandon som övergångsrelationer mellan tillstånd definierade genom logiska inferenssystem.

Kapitel åtta tar upp formell verifiering av program, där vi använder olika kalkyler för att säkerställa att program fungerar som de ska. Vi diskuterar Hoares kalkyl och Dijkstra’s predikattransformatorkalkyl och visar hur dessa metoder kan användas för att verifiera korrektheten av program och säkerställa att programmen fungerar som förväntat i olika scenarier. Här är begreppen korrekthet och terminering avgörande, och vi ger konkreta exempel på hur man verifierar dessa egenskaper genom att använda invarianter och terminationmått.

Kapitel nio behandlar de formella aspekterna av konkurrerande system och system med icke-deterministiskt beteende, som ofta förekommer i samtidiga eller reaktiva system. Dessa system beskrivs genom övergångssystem som definieras av logiska formler. För att ange egenskaper hos sådana system, utvidgas först-orderlogik till linjär tidslogik, och vi använder denna för att verifiera säkerhets- och liveness-egenskaper. Begreppet systeminvarianter, och hur dessa används för att bevisa systemets korrekthet, är centralt.

För att till fullo förstå och tillämpa de metoder som presenteras i denna bok är det avgörande att förstå den djupa kopplingen mellan logikens struktur och programmeringens praktik. Boken erbjuder en systematisk väg för att bygga en gedigen förståelse av dessa logiska verktyg, vilket gör det möjligt att skapa mer robust och säker programvara. Genom att förstå de teoretiska grunderna kan praktiska problem lösas effektivare och med större tillförlitlighet.

Endtext