Vi presenterar ett nytt tillvägagångssätt för exemple-guidad programsyntes baserad på motexempel-vägledd abstraktion förfining. Vår metod använder den abstrakta semantik av den underliggande DSL för att hitta ett program P vars abstrakt beteende uppfyller exemplen. Eftersom program P kan vara oäkta med avseende på de konkreta semantiken, förfinar vårt tillvägagångssätt iterativt abstraktionen tills vi antingen hittar ett program som uppfyller exemplen eller bevisar att inget sådant DSL-program existerar. Eftersom många program har samma input-output beteende i termer av deras abstrakta semantik, minskar denna syntes metod avsevärt sökytan jämfört med befintliga tekniker som använder rent betong semantik. Medan syntes med abstraktion förfining (SYNGAR) kan genomföras i olika inställningar, föreslår vi en förfining-baserad syntesalgoritm som använder abstrakt finita trädautomata (AFTA). Vår teknik använder en grov initial program abstraktion för att konstruera en inledande AFTA, som iterativt förfinas genom att bygga ett bevis på felaktighet av någon falsk program. Förutom att utesluta det falska program som accepterades av den tidigare AFTA, bevis på felaktighet är också användbara för att utesluta många andra falska program. Vi genomför dessa idéer inom en ram som kallas Blaze, som kan direktieras inom olika områden genom att tillhandahålla en lämplig DSL och dess motsvarande konkreta och abstrakta semantik. Vi har använt Blaze ramverket för att bygga synthesizers för sträng- och matrisomvandlingar, och vi jämför Blaze med befintliga tekniker. Våra resultat för strängdomänen visar att Blaze på ett gynnsamt sätt jämför med FlashFill, en domänspecifik synthesizer som nu används i Microsoft PowerShell. I samband med matrismanipuleringar jämför vi Blaze mot Prose, en toppmodern generell VSA-baserad synthesizer, och visar att Blaze resulterar i en 90x speed-up över Prose. Inom båda tillämpningsområdena förbättrar Blaze också konsekvent prestandan hos två andra befintliga tekniker i åtminstone en storleksordning. Abstract Synthesizer Checker Raffiner kandidatprogram Misslyckas (ingen lösning) Syntetiserade program counter exempel & falska program ny abstraktion Slutanvändare Domän expert Exempel DSL w / abstrakt semantik SYNGAR AFTA constr uction AST kommenteras med gamla abstrakta värden AST kommenteras med konkreta värden Pr oof constr uction Rank Predicates Pr oof constr uction Program: id(x) Program: id(x) + 2 Program: id(x) * 3 Predicates Program: (id(x) + 2) * 3 Iteration 1: Den konstruerade AFTA är A 1, Rank avkastning Π 1, Π 1 är sporrande, och beviset på felaktighet är I 1. AFTA constr uction AST kommenteras med gamla abstrakta värden AST kommenteras med konkreta värden Pr oof constr uction Rank Predicates 2 AST kommenteras med gamla abstrakta värden AST kommenteras med konkreta värden Pr oof constr uction Predicates 3 AST kommenteras med gamla abstrakta värden AST kommenteras med konkreta värden Pr oof constr uction Program: id(x) Program: id(x) + 2 Program: id(x) * 3 Predicates Program: (id(x) + 2) * 3 Iteration 2: Den konstruerade AFTA är A 2, Rank returnerar Π 2 är sporande, och beviset på felaktighet är I 2. AFTA constr uction AST kommenteras med gamla abstrakta värden AST kommenteras med konkreta värden Pr oof constr uction Rank Predicates 2 AST kommenteras med gamla abstrakta värden AST kommenteras med konkreta värden Pr oof constr uction Predicates 3 AST kommenteras med gamla abstrakta värden AST kommenteras med konkreta värden Pr oof constr uction Program: id(x) Program: id(x) + 2 Program: id(x) * 3 Predicates Program: (id(x) + 2) * 3 Iteration 3: Den konstruerade AFTA är A 3, Rank returnerar Π 3 är sporös, och beviset på felaktighet är I 3. AFTA constr uction AST kommenterade med gamla abstrakta värden AST kommenterade med konkreta värden Pr oof constr uction Rank Predicates 2 AST kommenterade med gamla abstrakta värden AST kommenterade med konkreta värden Pr oof constr uction Predicates 3 AST kommenterade med gamla abstrakta värden AST kommenterade med konkreta värden
SYNGAR REF använder predikerad abstraktion för att beskära sökytan för en syntes från exempel problem.
Program synthesis using abstraction refinement
{'venue': 'PACMPL', 'journal': None, 'mag_field_of_study': ['Computer Science']}