Att fastställa kvantitativa gränser för genomförandekostnaderna för program är viktigt inom många områden av datavetenskap såsom komplexitetsanalys, kompilatoroptimering, säkerhet och integritet. Tekniker baserade på programanalys, typsystem och abstrakt tolkning är välstuderade, men metoder för att analysera hur genomförandekostnaderna för två program jämförs med varandra har inte uppmärksammats. Naively kombinera de värsta och bästa fall genomförandekostnader för de två programmen fungerar inte bra i många fall eftersom en sådan analys glömmer likheterna mellan programmen eller indata. I detta arbete föreslår vi en relationell kostnadsanalysteknik som kan fastställa exakta gränser för skillnaden i utförandekostnad för två program genom att använda relationsegenskaper hos program och indata. Vi utvecklar RelCost, en förfining typ och effekt system för en högre ordning funktionellt språk med rekursion och subtyping. Den viktigaste nyheten i vår teknik är kombinationen av relationsförfiningar med två sätt att skriva-relationell maskinskrivning för resonemang om liknande beräkningar/inputs och unary typing för resonemang om orelaterade beräkningar/inputs. Denna kombination gör det möjligt för oss att analysera skillnaden i utförande kostnader för två program mer exakt än en naiv icke-relationell strategi. Vi bevisar vårt typsystem ljud med hjälp av en semantisk modell baserad på steg-indexerade unary och binära logiska relationer som står för icke-relationella och relations resonerande principer med deras respektive kostnader. Vi visar precisionen och generaliteten i vår teknik genom exempel.
Ett liknande tillvägagångssätt kan användas för att resonera om skillnaden i resursanvändning av två program REF.
Relational cost analysis
{'venue': 'POPL 2017', 'journal': None, 'mag_field_of_study': ['Computer Science']}