Whiley (programmeringsspråk)
| Paradigm | Imperativ , funktionell |
|---|---|
| Designad av | David J. Pearce |
| Dök först upp | juni 2010 |
| Stabil frisättning | 0.6.1 / 27 juni 2022
|
| Maskinskrivningsdisciplin | Stark , säker , strukturell , flödeskänslig |
| Licens | BSD |
| Hemsida | |
| Influerad av | |
| Java , C , Python , Rust | |
Whiley är ett experimentellt programmeringsspråk som kombinerar funktioner från de funktionella och imperativa paradigmen, och stöder formell specifikation genom funktionsförutsättningar , postvillkor och loopinvarianter . Språket använder flödeskänslig typning, även känd som "flödestypning".
Whiley-projektet startade 2009 som svar på "Verifying Compiler Grand Challenge" som presenterades av Tony Hoare 2003. Den första offentliga releasen av Whiley var i juni 2010.
Whiley är främst utvecklat av David Pearce och är ett projekt med öppen källkod med bidrag från ett litet samhälle. Systemet har använts för studentforskningsprojekt och i undervisningen i grundutbildningen. Det stöddes mellan 2012 och 2014 av Royal Society of New Zealands Marsden Fund.
Whiley-kompilatorn genererar kod för den virtuella Java-maskinen och kan samverka med Java och andra JVM-baserade språk.
Översikt
Målet med Whiley är att tillhandahålla ett realistiskt programmeringsspråk där verifiering används rutinmässigt och utan eftertanke. Idén med ett sådant verktyg har en lång historia, men främjades starkt i början av 2000-talet genom Hoares Verifying Compiler Grand Challenge. Syftet med den här utmaningen var att stimulera nya ansträngningar för att utveckla en verifierande kompilator , ungefär beskrivet enligt följande:
En verifierande kompilator använder matematiska och logiska resonemang för att kontrollera riktigheten av de program som den kompilerar.
— Tony Hoare
Det primära syftet med ett sådant verktyg är att förbättra mjukvarans kvalitet genom att se till att ett program uppfyller en formell specifikation . Whiley följer många försök att utveckla sådana verktyg, inklusive anmärkningsvärda insatser som SPARK/Ada , ESC/Java , Spec#, Dafny , Why3 och Frama-C .
De flesta tidigare försök att utveckla en verifierande kompilator fokuserade på att utöka befintliga programmeringsspråk med konstruktioner för att skriva specifikationer. Till exempel, ESC/Java och Java Modeling Language lägger till kommentarer för att specificera förutsättningar och eftervillkor till Java . På samma sätt lägger Spec# och Frama-C till liknande konstruktioner till programmeringsspråken C# och C. Men dessa språk är kända för att innehålla många funktioner som ställer till svåra eller oöverstigliga problem för verifiering. Däremot utformades Whiley-språket från grunden i ett försök att undvika vanliga fallgropar och göra verifieringen mer lätthanterlig.
Funktioner
Syntaxen för Whiley följer det allmänna utseendet hos imperativa eller objektorienterade språk. Indragningssyntax väljs framför användningen av klammerparenteser för att avgränsa satsblock, med tanke på en stark likhet med Python . Det imperativa utseendet på Whiley är dock något missvisande eftersom språkkärnan är funktionell och ren .
Whiley skiljer en funktion (som är ren ) från en metod (som kan ha biverkningar ). Denna distinktion är nödvändig eftersom den gör att funktioner kan användas i specifikationer. En välbekant uppsättning primitiva datatyper är tillgängliga inklusive bool , int , arrayer (t.ex. int[] ) och poster (t.ex. {int x, int y} ) . Men till skillnad från de flesta programmeringsspråk är heltalsdatatypen, int , obegränsad och motsvarar inte en representation med fast bredd som 32-bitars tvåkomplement . Således kan ett obegränsat heltal i Whiley anta alla möjliga heltalsvärden, med förbehåll för värdmiljöns minnesbegränsningar. Detta val förenklar verifieringen, eftersom resonemang om modulo-aritmetik är ett känt och svårt problem. Sammansatta objekt (t.ex. arrayer eller poster) är inte referenser till värden på heapen som de är i språk som Java eller C# utan är istället oföränderliga värden.
Whiley har ett ovanligt tillvägagångssätt för typkontroll som kallas "Flow Typing". Variabler kan ha olika statiska typer vid olika punkter i en funktion eller metod. Flödestypning liknar förekomsttypning som finns i Racket . För att underlätta flödestypning stöder Whiley förenings- , korsnings- och negationstyper. Unionstyper är jämförbara med summatyper som finns i funktionella språk som Haskell , men i Whiley är de inte osammanhängande. Skärnings- och negationstyper används i samband med flödestypning för att bestämma typen av en variabel på de sanna och falska grenarna av ett körtidstyptest. Anta till exempel att en variabel x av typ T och ett körtidstyptest x är S . På den sanna grenen blir typen av x T & S medan den på den falska grenen blir T & !S .
Whiley använder ett strukturellt snarare än nominellt system. Modula-3 , Go och Ceylon är exempel på andra språk som stöder strukturell typning i någon form.
Whiley stöder referenslivslängder liknande de som finns i Rust . Livstider kan anges vid allokering av nya objekt för att indikera när de säkert kan deallokeras. Referenser till sådana objekt måste då inkludera livstidsidentifierare för att förhindra dinglande referenser . Varje metod har en implicit livslängd som avses med detta . En variabel av typen &this:T representerar en referens till ett objekt av typen T som tilldelas den omslutande metoden. Subtypning mellan livstider bestäms av livslängdsrelationen . Sålunda &l1:T en undertyp av &l2:T om livstid l1 statiskt överlever livstid l2 . En livstid vars omfattning omsluter en annan sägs överleva den. Livstider i Whiley skiljer sig från Rust genom att de för närvarande inte inkluderar ett begrepp om ägande .
Whiley har inget inbyggt stöd för samtidighet och ingen formell minnesmodell för att bestämma hur läsning/skrivning till delat föränderligt tillstånd ska tolkas.
Exempel
Följande exempel illustrerar många av de intressanta funktionerna i Whiley, inklusive användningen av postvillkor, loopinvarianter, typinvarianter, unionstyper och flödestypning. Funktionen är avsedd att returnera det första indexet för ett heltalsobjekt i en array av heltalsobjekt . Om inget sådant index finns, returneras null .
0
0
0
0
0
// Definiera typen av naturliga tal typ nat är ( int x ) där x >= public function indexOf ( int [] items , int item ) -> ( int | null index ) // Om int returneras, matchar element vid denna position objekt säkerställer att index är int ==> objekt [ index ] == objekt // Om int returneras, element vid denna position är första matchningen säkerställer att index är int ==> nej { i i .. index | objekt [ i ] == objekt } // Om null returneras, matchar inget element i objekt objektet säkerställer att index är null ==> nej { i i .. | föremål | | objekt [ i ] == objekt } : // nat i = // medan i < | föremål | // Inget element sett hittills matchar objekt där ingen { j i .. i | objekt [ j ] == objekt } : // om objekt [ i ] == objekt : returnera i i = i + 1 // return null
I ovanstående ges funktionens deklarerade returtyp unionstypen int|null som indikerar att antingen ett int- värde returneras eller null returneras. Funktionens postcondition består av tre säkerställer -satser, som var och en beskriver olika egenskaper som måste hålla för det returnerade indexet . Flödestypning används i dessa klausuler genom runtime-typtestoperatören, är . Till exempel, i den första försäkrar- satsen, skrivs variabelindexet om från int|null till just int på höger sida om implikationsoperatorn (dvs == > ).
Ovanstående exempel illustrerar också användningen av en induktiv loopinvariant . Slingans invariant måste visas för att hålla vid inträde i slingan, för varje given iteration av slingan och när slingan går ut. I det här fallet anger loopinvarianten vad som är känt om elementen i de objekt som har undersökts hittills - nämligen att ingen av dem matchar det givna objektet . Slinginvarianten påverkar inte innebörden av programmet och kan i någon mening anses onödig. Men slinginvarianten krävs för att hjälpa den automatiserade verifieraren som använder i Whiley-kompilatorn att bevisa att denna funktion uppfyller dess specifikation.
Ovanstående exempel definierar också typen nat med en lämplig typinvariant . Denna typ används för att deklarera variabel i och indikera att den aldrig kan hålla ett negativt värde. I det här fallet förhindrar deklarationen behovet av en extra loopinvariant av formen där i >= 0 som annars skulle vara nödvändigt.
Historia
Whiley började 2009 med den första offentliga utgåvan, v0.2.27 som följde i juni 2010 och v0.3.0 i september samma år. Språket har utvecklats långsamt med många syntaktiska förändringar som gjorts hittills. Versioner före v0.3.33 stödde förstklassiga sträng- och char -datatyper, men dessa togs bort till förmån för att representera strängar som begränsade int[]- matriser. På samma sätt stödde versioner före v0.3.35 förstklassig uppsättning (t.ex. {int} ), ordbok (t.ex. {int=>bool} ) och storleksändringsbar lista [int] ), men dessa togs bort till förmån för enkla arrayer (t.ex. int [] ). Det kanske mest kontroversiella var borttagandet av den riktiga datatypen i version v0.3.38 . Många av dessa förändringar motiverades av en önskan att förenkla språket och göra kompilatorutvecklingen mer hanterbar.
En annan viktig milstolpe i utvecklingen av Whiley kom i version v0.3.40 med införandet av referenslivslängder, utvecklad av Sebastian Schweizer som en del av hans masteruppsats vid universitetet i Kaiserslautern .