Abstract Sketching är en syntesmetod som syftar till att överbrygga klyftan mellan en programmerares insikter på hög nivå om ett problem och datorns förmåga att hantera detaljer på låg nivå. Vid skissning använder programmeraren ett partiellt program, en skiss, för att beskriva den önskade genomförandestrategin, och lämnar detaljerna på låg nivå i genomförandet till ett automatiserat syntesförfarande. För att generera ett genomförande från programmeraren som tillhandahålls skiss, använder synthesizer kontraexempel-vägledd induktiv syntes (CEGIS). Induktiv syntes avser processen att generera kandidatimplementeringar från konkreta exempel på korrekt eller felaktigt beteende. CEGIS kombinerar en SAT-baserad induktiv synthesizer med ett automatiserat valideringsförfarande, en begränsad modellkontroll, som kontrollerar om kandidatgenomförandet som produceras genom induktiv syntes verkligen är korrekt och att ta fram nya motexempel. Resultatet är en syntes procedur som kan hantera komplexa problem från en mängd olika domäner inklusive chiffer, vetenskapliga program, och även samtidiga data-strukturer.
CounterExemple-Guided Inductive Synthesis (CEGIS) REF infördes som en teknik för att lösa D@-queries med en tillämpning på parametersyntes i skisser av program.
Program sketching
{'venue': 'International Journal on Software Tools for Technology Transfer', 'journal': 'International Journal on Software Tools for Technology Transfer', 'mag_field_of_study': ['Computer Science']}