Bibliotek med effektiva datatyper och algoritmer
The Library of Efficient Data types and Algorithms ( LEDA ) är ett proprietärt licensierat programvarubibliotek som tillhandahåller C++ -implementeringar av ett brett utbud av algoritmer för grafteori och beräkningsgeometri . Det utvecklades ursprungligen av Max Planck Institute for Informatics Saarbrücken . Sedan 2001 vidareutvecklas och distribueras LEDA av Algorithmic Solutions Software GmbH.
LEDA finns tillgänglig som gratis, forskning och professionell utgåva. Gratisutgåvan är gratisprogram , med tillgång till källkod tillgänglig för köp. Research och Professional-utgåvorna kräver betalning av licensavgifter för all användning. Sedan oktober 2017 är LEDA-grafalgoritmer också tillgängliga för Java-utvecklingsmiljön .
Tekniska detaljer
Datatyper
Numeriska representationer
LEDA tillhandahåller ytterligare fyra numeriska representationer vid sidan av de inbyggda i C++: heltal , rationell , bigfloat och real :
- LEDA:s
heltalstyperbjuder en förbättring jämfört med den inbyggdaint-datatypen genom att eliminera problemet med spill till bekostnad av obegränsad minnesanvändning för allt större antal. - Det följer att LEDA:s
rationellatyp har samma motstånd mot översvämning eftersom den är baserad direkt på den matematiska definitionen av rationell som kvoten av tvåheltal. - Bigfloat -typen förbättras jämfört med C++ flyttalstyperna genom att tillåta mantissa att ställas in på en godtycklig precisionsnivå istället för att följa IEEE
-standarden . - LEDA:s
verkligatyp möjliggör exakta representationer av reella tal och kan användas för att beräkna tecknet för ett radikalt uttryck.
Fel vid kontroll
LEDA använder sig av certifieringsalgoritmer för att visa att resultaten av en funktion är matematiskt korrekta. Förutom inmatning och utmatning av en funktion, beräknar LEDA ett tredje "vittne"-värde som kan användas som indata till kontrollprogram för att validera utdata från funktionen. LEDA:s kontrollprogram utvecklades i Simpl, ett imperativt programmeringsspråk , och validerades med hjälp av Isabelle/HOL , ett mjukvaruverktyg för att kontrollera korrektheten av matematiska bevis.
Typen av ett vittnesvärde beror ofta på vilken typ av matematisk beräkning som utförs. För LEDA:s planaritetstestfunktion, Om grafen är plan , produceras en kombinatorisk inbäddning som ett vittne. Om inte, returneras en Kuratowski-subgraf . Dessa värden kan sedan skickas direkt till kontrollfunktioner för att bekräfta deras giltighet. En utvecklare behöver bara förstå det inre av dessa kontrollfunktioner för att vara säker på att resultatet är korrekt, vilket avsevärt minskar inlärningskurvan jämfört med att få en fullständig förståelse för LEDA:s planaritetstestningsalgoritm.
Användningsfall
LEDA är användbar inom området beräkningsgeometri på grund av dess stöd för exakta representationer av reella tal via datatypen leda_real . Detta ger en fördel i noggrannhet jämfört med flyttalsaritmetik . Till exempel är beräkningar som involverar radikaler betydligt mer exakta när de beräknas med leda_real . Algoritmer som parametrisk sökning , en teknik för att lösa en delmängd av optimeringsproblem och andra under den verkliga RAM -modellen för beräkning förlitar sig på reella talparametrar för att ge korrekta resultat.
Alternativ
Boost och LEMON är potentiella alternativa bibliotek med vissa fördelar i effektivitet på grund av olika implementeringar av grundläggande algoritmer och datastrukturer. Ingen av dem använder dock en liknande uppsättning korrekthetskontroller, särskilt när det handlar om aritmetik med flyttal.
externa länkar