Hume (programmeringsspråk)
Hume är ett funktionellt baserat programmeringsspråk som utvecklats vid University of St Andrews och Heriot-Watt University i Skottland sedan år 2000. Språknamnet är både en akronym som betyder "Higher-order Unified Meta-Environment" och en hedersbetygelse för 1700-talet filosofen David Hume . Det är inriktat på inbyggda system i realtid , som syftar till att producera en design som både är mycket abstrakt, men som ändå tillåter exakt extraktion av kostnader för tid och utrymme. Detta gör att programmerare kan garantera de begränsade tids- och utrymmeskraven för att köra program.
Hume kombinerar funktionella programmeringsidéer med idéer från finita tillståndsautomater . Automater används för att strukturera kommunicerande program i en serie "boxar", där varje ruta mappar ingångar till utgångar på ett rent funktionellt sätt med hjälp av högnivåmönstermatchning. Den är strukturerad som en serie nivåer, som var och en exponerar olika maskinegenskaper.
Designmodell
Hume-språkdesignen försöker bibehålla de väsentliga egenskaperna och funktionerna som krävs av domänen för inbäddade system (särskilt för transparenta tids- och rumskostnader) samtidigt som den innehåller en så hög grad av programabstraktion som möjligt. Det syftar till att rikta in sig på applikationer som sträcker sig från enkla mikrokontroller till komplexa realtidssystem som smartphones . Detta ambitiösa mål kräver inkorporering av både lågnivåbegrepp som avbrottshantering och högnivåer av datastrukturabstraktion etc. Naturligtvis kommer sådana system att programmeras på vitt skilda sätt, men språkdesignen bör tillgodose dessa varierande krav.
Hume är ett språk i tre lager: ett yttre (statiskt) deklarations-/ metaprogrammeringslager , ett mellanliggande koordinationslager som beskriver en statisk layout av dynamiska processer och tillhörande enheter, och ett inre lager som beskriver varje process som en (dynamisk) mappning från mönster till uttryck. Det inre lagret är statslöst och rent funktionellt.
Istället för att försöka tillämpa kostnadsmodellering och korrekthetsbevisande teknologi på ett befintligt språkramverk antingen direkt eller genom att ändra ett mer allmänt språk (som med t.ex. RTSJ ), är Hume-designernas tillvägagångssätt att designa Hume på ett sådant sätt att formella modeller och bevis kan definitivt konstrueras. Hume är uppbyggd som en serie av överlappande språknivåer, där varje nivå lägger till uttryckbarhet till uttryckets semantik, men antingen förlorar någon önskvärd egenskap eller ökar den tekniska svårigheten att tillhandahålla formella korrekthets-/kostnadsmodeller.
Egenskaper
Tolk- och kompilatorversionerna skiljer sig lite åt.
- tolken (konceptbevisare) medger timeout och anpassade undantag.
- kompilatorn tillåter heap- och stackkostnadsbegränsning men undantag skriver bara ut undantagsnamnet.
Koordinationssystemet kopplar lådor i en dataflödesprogrammeringsstil .
Uttrycksspråket är Haskell -likt.
Meddelandet som passerar samtidighetssystemet minns JoCamls Join-mönster eller Polyphonic C Sharp- ackord , men med alla kanaler asynkrona .
Det finns en schemaläggare inbyggd som kontinuerligt kontrollerar mönstermatchning genom alla rutor i tur och ordning, och ställer in de rutor som inte kan kopiera utdata till upptagna indatadestinationer.
Exempel
Försäljningsautomat
0
0
data Mynt = Nickel | Dime | Fake ; data Drycker = Kaffe | Te ; dataknappar = BCaffe | _ BTea | BCavbryt ; typ Int = int 32 ; undantag EFakeCoin :: ( Int , sträng ) ; visa v = v som sträng ; box kaffe in ( mynt :: Mynt , knapp :: Knappar , värde :: Int ) -- ingångskanaler ut ( drink_outp :: sträng , värde ' :: Int , refund_outp :: sträng , display :: sträng ) -- namngivna utgångar inom 500 KB ( 400 B ) -- max heap ( max stack ) kostnadsbegränsande handtag EFakeCoin , TimeOut , HeapOverflow , StackOverflow match -- * jokertecken för ofyllda utdata och outnyttjade ingångar ( my_coin , * , v ) {- ''join- mönster'' ekvivalent: mynt(mitt_mynt) & värde(v) -} -> låt v ' = ökaKredit mitt_mynt v in ( * , v ' , * , visa v ' ) -- tidsgränsande (''inom x tidsenhet '') höjer TimeOut () | ( * , BCoffee , v ) {- ''join-pattern'' ekvivalent: button(BCoffee) & value(v) -} - > ( vend Coffee 10 v ) inom 30 s | ( * , BTea , v ) -> ( säljer Tea 5 v ) inom 30 s | ( * , BCancel , v ) -> let refund u = "Återbetalning " ++ visa u ++ " \n " i ( * , , refund v , * ) handtag EFakeCoin ( v , msg ) -> ( * , v , * , msg ) | TimeOut () -> ( * , * , * , "kanske innehållet är slut, ring service!" ) | HeapOverflow () -> ( * , * , * , "fel: höggränsen har överskridits" ) | StackOverflow () -> ( * , * , * , "fel: stackgränsen har överskridits" ) ; inkrementKreditmynt v = fallmynt av Nickel -> v + 5 Dime -> v + 10 Fake - > höj EFakeCoin ( v , "mynt avvisat " ) ; vend dryck kostar v = om v >= kostar då ( servera drink , v - kostnad , * , "din drink" ) else ( * , v , * , "pengar saknas " ++ visa ( kostnad - v )) ; servera dryck = kaffedryck -> "Kaffe \ n " Te -> " Te \ n " ; boxkontroll in ( c :: char ) ut ( mynt :: Mynt , knapp :: Knappar ) matcha 'n' - > ( Nickel , * ) | 'd' -> ( Dime , * ) | 'f' -> ( Fake , * ) | 'c' -> ( * , BCoffe ) | 't' -> ( * , BTea ) | 'x' -> ( * , BCancel ) | _ -> ( * , * ) ; streama console_outp till "std_out" ; streama console_inp från "std_in" ; -- dataflödestråd kaffe -- ingångar ( kanal ursprung ) ( kontroll . mynt , kontroll . knapp , kaffe . värde ' initialt ) -- -- utgång destinationer ( console_outp , coffee . value , console_outp , console_outp ) ; trådkontroll ( console_inp ) ( kaffe . mynt , kaffe . knapp ) ; _
externa länkar
- Webbplatsen för Hume Programming Language
- Hume-projektet vid Heriot-Watt University
- Inbäddad funktionell programmering i Hume Document
- EmBounded-projektet Projekt för att certifiera resursbunden kod i Hume.
- Hume och Multicore