Kompilatorns korrekthet

Inom databehandling är kompilatorns korrekthet den gren av datavetenskap som handlar om att försöka visa att en kompilator beter sig enligt sin språkspecifikation . Tekniker inkluderar att utveckla kompilatorn med formella metoder och använda rigorösa tester (ofta kallade kompilatorvalidering) på en befintlig kompilator.

Formell verifiering

Två huvudsakliga formella verifieringsmetoder för att fastställa kompileringens korrekthet är att bevisa att kompilatorn är korrekt för alla indata och att bevisa riktigheten av en kompilering av ett visst program (översättningsvalidering).

Kompilatorns korrekthet för alla inmatningsprogram

Kompilatorvalidering med formella metoder involverar en lång kedja av formell, deduktiv logik . Men eftersom verktyget för att hitta beviset ( satsbevis ) är implementerat i mjukvara och är komplext, är det stor sannolikhet att det kommer att innehålla fel. Ett tillvägagångssätt har varit att använda ett verktyg som verifierar beviset (en proof checker ) som, eftersom det är mycket enklare än en proof-finder, är mindre sannolikt att innehålla fel.

Ett framträdande exempel på detta tillvägagångssätt är CompCert , som är en formellt verifierad optimeringskompilator av en stor delmängd av C99 .

En annan verifierad kompilator utvecklades i CakeML-projektet, som fastställer riktigheten av en betydande delmängd av standard ML- programmeringsspråk med hjälp av HOL (proof assistant) .

Ett annat tillvägagångssätt för att få en formellt korrekt kompilator är att använda semantikstyrd kompilatorgenerering.

Översättningsvalidering: kompilatorns korrekthet på ett givet program

I motsats till att försöka bevisa att en kompilator är korrekt för alla giltiga inmatningsprogram syftar översättningsvalidering till att automatiskt fastställa att ett givet inmatningsprogram är korrekt kompilerat. Att bevisa korrekt kompilering av ett givet program är potentiellt lättare än att bevisa att en kompilator är korrekt för alla program, men kräver fortfarande symboliska resonemang, eftersom ett fast program fortfarande kan fungera på godtyckligt stora ingångar och köras under en godtyckligt lång tid. Översättningsvalidering kan återanvända en befintlig kompilatorimplementering genom att generera, för en given kompilering, ett bevis på att kompileringen var korrekt. Översättningsvalidering kan användas även med en kompilator som ibland genererar felaktig kod, så länge denna felaktiga inte visar sig för ett givet program. Beroende på inmatningsprogrammet kan översättningsvalideringen misslyckas (eftersom den genererade koden är fel eller att översättningsvalideringstekniken är för svag för att visa korrekthet). Men om översättningsvalideringen lyckas, är det kompilerade programmet garanterat korrekt för alla indata.

Testning

Testning representerar en betydande del av ansträngningen för att skicka en kompilator, men får jämförelsevis lite täckning i standardlitteraturen. 1986 års upplaga av Aho, Sethi, & Ullman har ett ensidigt avsnitt om kompilatortestning, utan några namngivna exempel. 2006 års utgåva utelämnar avsnittet om testning, men understryker dess betydelse: ”Optimering av kompilatorer är så svåra att få till rätt att vi vågar påstå att ingen optimeringskompilator är helt felfri! Det viktigaste syftet med att skriva en kompilator är alltså att den är korrekt.” Fraser & Hanson 1995 har ett kort avsnitt om regressionstestning ; källkoden är tillgänglig. Bailey & Davidson 2003 omslagstestning av proceduranrop Ett antal artiklar bekräftar att många släppta kompilatorer har betydande kodkorrekthetsbuggar. Sheridan 2007 är förmodligen den senaste tidskriftsartikeln om allmän kompilatortestning. För de flesta ändamål är den största mängden information som finns tillgänglig om kompilatortestning Fortran- och Cobol-valideringssviterna.

Ytterligare vanliga tekniker när man testar kompilatorer är fuzzing (som genererar slumpmässiga program för att försöka hitta buggar i en kompilator) och testfallsreduktion (som försöker minimera ett hittat testfall för att göra det lättare att förstå).

Se även

• Kompilator
• Verifiering och validering (mjukvara)
• Korrekthet (datavetenskap)
• CompCert C-kompilator — Formellt verifierad C-kompilator
• Reflektioner om tillit till tillit