133
considerfirstsynthesizingprogramswherea singlecascadingse-
quenceof if...else if...elseexpressionsoccuratthe top-
levelofthefunctionbody,witheachbranchnotcontainingcondi-
tionals.Thenthegoalistohaveasfewbranchesintheonetop-level
conditional aspossible.Theproblemistopartitionthe examples
intowhich-branch-handles-themtoachievethisgoal.
Foreveryprogramp DBS tries,thesetofexamplesithandles
correctlyisrecordedandcalledT(p).IfT(p)=S (allexamples
handled),p isacorrect solution andcanbe returned. Otherwise,
eachsetofprogramsQ(wherejQjm)whoseunionofhandled
examples
S
p2Q
T(p)equalsS isacandidate forasolutionwith
appropriateconditionals.Tobeasolution,Qalsoneedsguardsthat
leadexamplestoabranchthatisvalidforthem; tosimplifythis,
wheneverabooleanexpressiongisgenerated,thesetofexamples
itreturnstruefor,B(g),isrecorded.ThesetsQareconsideredin
orderofincreasingsize,soiftherearemultiplesolutions,theone
withthefewestbrancheswillbechosen.
Iftheconditionaldoesnotappearatthetop-level,thenitmust
appearastheargumenttosomefunction.Tohandlethiscase,we
notethatifeverybranchoftheconditionalgeneratedasdescribed
already happensto contain a call to a function f with different
arguments,thenitcouldberewrittensuchthatthecalltof occurs
outsideoftheconditionalifthatisallowedbytheDSL.Inthatcase,
wecansaythatallofthebranchesmatchthecontextf().
In the algorithm, for each non-terminal the DSL allows for
conditionalsat, eachprogram pisput into zero ormore buckets
labeledwiththecontextthatnon-terminalappearsin.Forexample,
iftheargumentoffmaybeaconditionalandp=f(f(x))thenp
wouldbeputinthebucketsforf()andf(f()).Thenthesame
algorithm asabove isrun for eachbucket with the conditionals
being rewritten to appear inside the context. Inserting multiple
conditionalsjustinvolvesfollowingthislogicmultipletimes.
5.3 Loops
TheprimarywayDBS handlesloopsistosimplynotdoanything
specialatall:recursionandcallinghigher-orderfunctionslikemap
and fold are handled by the algorithm asdescribed so far. As
describedin§3.2,ageneralWhileLoophigher-orderfunctioncan
beusedtoexpressarbitraryloopsthatDBSmaysynthesizelikeany
otherDSL-definedfunction.Onthe otherhand,theuse ofloops
incodeoftencorrespondstopatternsintheinput/outputexamples.
Thissectiondiscussestwosuchcommonpatternswehavewritten
strategiesfor;expertsdesigningDSLsmayadditionallydefinetheir
ownstrategiesforotherformsofloops.
ThesecanbeusedinaDSLviathe
FOREACH(
)or
FOR(
)
ruleswhereEisthenon-terminalforthebodyoftheloop.
Foreach The“foreach”loopstrategy’shypothesisisthatthereis
a1-to-1correspondencebetweenaninputarrayandanoutputarray.
Assumingthathypothesis,theexamplescanbesplitintooneexam-
pleforeachelementwhereiistheindex,currentistheelement
atthatindex,andaccisthearrayofoutputsforpreviousindexes:
(in =f3;5;4g;RET =f9;25;16g)wouldbecometheexamples
(in = f3;5;4g;i = 0;current = 3; acc = fg;RET = 9),
(in = f3;5;4g;i = 1;current = 5;acc = f3g;RET = 25),
and(in=f3;5;4g;i=2;current=4;acc=f9;25g;RET=
16). Those examplescouldbeusedtosynthesize theloopbody
current*current using TDS. The strategy includes the boiler-
plate code to take the loop bodycurrent*current andoutput
aforeachloopovertheinputarray.
Thatexampleisoverlysimpleassuchacomputationcouldeas-
ilybecapturedbyamap.However,loopstrategiesalsoallowfor
loopsthatarenotaseasilyexpressedwithhigher-orderfunctions.
Forexample,theloopbodiesexamplescouldalsoincludetheval-
uescomputedsofar:(in=f5;2;3g;RET=f5;7;10g)wouldbe-
come(in=f5;2;3g;i=0;current=5;acc=fg;RET=5),
(in=f5;2;3g;i=1;current=2;acc=f5g;RET=7),and
(in=f5;2;3g;i=2;current=3;acc=f5;7g;RET=10).
Then the synthesized loop body would be acc.Length > 0 ?
current + acc.Last() : current,whichcouldbe rewritten
intoaloopcomputingthecumulativesumofin.
For Patternsmay also showup across examples.Forinstance,
giventheexamples(in=0;RET=0);(in=1;RET=1);(in=
2;RET = 3);(in = 3;RET = 6)we cansee,lookingacrossex-
amples,that for eachinput value the result shouldbe the result
forthe previousinput value plus the newinput (which isanin-
direct way of saying “sum the numbersup to in”).In terms of
loopstrategies,thehypothesisisthatpairsofexampleswherethe
input in differby one correspond to adjacent loop iterations so
bycombiningthosepairswecangetexamplesfortheloopbody
where i is current value of the loop iterator and acc is the re-
turnvalueof the i 1iteration: (i = 1;acc = 0;RET = 1),
(i = 2;acc = 1;RET = 3),and(i = 3;acc = 3;RET = 6).
ThenTDSwillgivei + accfortheloopbody.Theloopstrategy
willidentifythat(in=0;RET=0)indicatesthattheloopiterator
shouldstartat0andtheaccumulatorshouldstartat0andproducea
forloopfor(int i = 1; i <= in; i++) acc = i + acc;.
Otherstrategies Different loop strategiescangive different in-
formationlikeincludingtheindexinaforeachorgivingacccor-
respondingtogoinginreverseorder.Furthermore,theconcept of
splitinguparraysbyelementtofindpatternscanalsobeappliedto
splittingstrings(bylengthordelimiters),XMLnodes,orwhatever
otherstructureddatamaybeinthetargetdomain.
5.4 Conditionalsandloops,ageneraltheory
DSLdefinitionscontainruleswithandwithoutspecializedstrate-
gies.Mostrules,includingallDSL-definedfunctions,donothave
specializedstrategiessoexpressionsusingthoserulesarebuiltus-
ingthedefaultstrategyofsearchingthroughthesemanticallydis-
tinctexpressions(usingtheexampleinputstodecidewhichexpres-
sionsare distinguishable).Onotherotherhand, we havedefined
strategiesforconditionalsandloopsthatusetheexampleoutputs
aswellastheinputstopowermoredirectedapproachestolearning
thoseconstructs.Whilewereferencedtheoutputvaluesdirectlyin
theexplanationofthestrategiesforloops,thediscussionofcondi-
tionalsonlyreferencedthemindirectlybykeepingtrackofwhich
examplesaprogramwascorrectfor.
Thestrategiesforconditionalsandloopsshouldbeconsidered
asjust different instancesofthesameconcept. Whilecondition-
alsmerelyselectasubsetofthe examplesforeachbranch,loops
dolarger rewritesof the examplesusedinthe recursive callsto
thesynthesizer.Theoretically,aDSLdesignercouldincludeother
strategieslikeinversesofDSL-definedfunctionsorapolynomial
solverfor synthesizing arithmetic. We presentlyomit suchfunc-
tionalitybecausewe believeit placesundue burdenon the DSL
designerbutintendtoinvestigateitinfuturework.
6. Evaluation
OurevaluationdemonstratesthatTDSissufficientlypowerfuland
generaltosynthesizenon-trivial—albeitsmall—programsinmul-
tiple domainsfrom small sequences of real world examples ob-
tainedfromhelpforums.WealsocompareTDStotoSketch[30],
thepresentstate-of-the-artindomain-agnosticprogramsynthesis,
andtostate-of-the-artspecializedsynthesizerswhereapplicable.
Furthermore,weexploredhowsensitiveouriterativesynthesis
techniqueactuallyistothepreciseorderingofexamples,showing
that exampleorder issignificant tospeedor abilitytosynthesize
ona non-trivial proportion oftheexamples, especiallyon larger
programs.Wealsovalidatedsomeofourdesigndecisionsbyse-
lectivelydisablingpartsofouralgorithm.
122
AllexperimentswererunonamachinewithaquadcoreIntel
XeonW35202.66GHzprocessorand6GBofRAM.
§6.1describesthebenchmarksusedinourexperimentandour
successinsynthesizingthemandcomparesTDStopriorspecialized
synthesizerswhereapplicable.§6.2investigatestheeffectofexam-
ple ordering to our synthesizer’sperformance. §6.3breaksdown
theusefulnessofthedifferentpartsofouralgorithm.§6.4evaluates
performanceforoursynthesizerandvalidatesourtimeoutchoice.
6.1 Benchmarks
We evaluateourtechnique infourdomains:§6.1.1comparesour
techniquetoastate-of-the-artspecializedprogrammingbyexample
systemforstringtransformations,§6.1.2comparesourtechnique
to astart-of-the-art specializedprogramming by example system
fortabletransformations,§6.1.3discussesusingoursystemforthe
noveldomainofXMLtransformations,whilefinally§6.1.4shows
ourtechniqueisabletoautomatecodinginTDDforintroductory
programmingproblems.
Forthefirstthree,theexamplesequencesusedandoutputofour
synthesizer can be found at https://homes.cs.washington.
edu/
~
perelman/publications/pldi14-tds.zip;thelastsec-
tion’sprogramsarenotpublic.
6.1.1 Stringtransformations
Stringtransformationprogramstake asinputoneormorestrings
andoutputastringconstructedfromtheinput usingmainlysub-
stringandconcatenationoperations.
Stringsareanaturalformatforinput/outputexamplesthatoften
appearin real-world end-userprogrammingtasksasrecentwork
byGulwanietal.[6]hasshown:theirworkbecametheFlashFill
featureinExcel2013[1].UnlikeFlashFill,TDSdoesnotusecareful
reasoningaboutthedomainofstrings,butitisstillabletoquickly
synthesize many of the same examples as well assome similar
programsthatthepriorwork(i.e.,FlashFill)cannotsynthesize.
Benchmarks Tocompareagainst FlashFill, we firstdefinedex-
actly the FlashFill DSL in our DSL definition language and ran
oursynthesizerontheexampleswhichappearin[6]toconfirmwe
couldsynthesizethem.Thenwemadeafewmodificationstothe
DSL whichare showninFig. 6tomakeit more general;specif-
ically,we allowed nested substringoperations,substring indexes
dependentontheloopvariable,andcallstootherLaSyfunctions.
InadditiontoWordWrapandtheexamplesfrom[6]wewrote
testcasesequencesfor7simplerealworldstringmanipulationex-
amplesoutside ofthe scope of FlashFill but handled byour ex-
tendedDSLincludingselectingthetwodigityearfromadate(re-
quiresnestedsubstrings),reversingastring(requiressubstringin-
dexesdependentontheloopvariable),andbibliographyexamples
liketheoneinFig.2(requiresauser-definedlookup).
Results Eachofthe15examplesequencescontains1–8examples
exceptforwordwrapwhichuses24examples.5oftheexamples
canbe synthesizedinunderasecond.6take morethan1second
butunder5seconds,whiletheother4finishinunder25seconds.
FlashFillsynthesizesalloftheexamplesitcanhandleinwellunder
asecond.SimplybyspecifyingtheDSL,ourdomain-agnosticsyn-
thesistechniquenearstheperformanceofastate-of-the-artspecial-
izedsynthesistechniquewhilemaintainingtheabilitytogenerate
morecomplicatedcontrolflowstructures.
WecodedallexamplesusingthecorrespondingDSLsinSketch
andnoneofthemcompletedwithin10minutes.
6.1.2 Tabletransformations
Tabletransformationsconvertspreadsheettablesbetweendifferent
formatsbyrearrangingandcopyingatable’scells.
Benchmarks [11]givesaDSLandsynthesisalgorithmforthese
transformationsalongwithacollectionofbenchmarkstheauthors
foundononlinehelpforums.WedefinedtheirDSLforoursynthe-
sizerandranitontheirbenchmarks.
Foradditionalbenchmarksnothandledby[11]weaddedmore
predicates to the grammar to allow it to handle a wider range
ofrealworldnormalizationscenarios.Forexample,ourextended
grammarcansupportconvertingvariousnon-standardspreadsheets
withsubheadersintonormalizedrelationaltables.
Results Eachofthe8benchmarksuses1–6examples.TDSsyn-
thesizesmostoftheminunder10seconds;2take30secondsand
onetakesafullminute.
[11]saysSketchwasunabletosynthesizetheirbenchmarksso
wedidnotattempttorunthebenchmarksusingSketch.
6.1.3 XMLtransformations
XMLtransformationsinvolvesomecombinationofmodifyingan
XMLtreestructureandtagattributesandstringtransformationson
thecontentoftheXMLnodes.
Benchmarks Weselected10differentrealworldexamplesfrom
online help forums and constructed a DSL able to express the
operationsnecessarytosynthesizeprogramsforallofthem.Two
oftheexamplesappearin§2.2.
Onetransformationinvolvedputtinga tagaroundeveryword,
evenwhenwordshadtagswithinthem,whichwaseasiesttoex-
presstreating the words as strings instead of as XML. Making
thestringandXMLDSLsworktogetherrequiredsimplyputting
the functionsto convert betweenthe two in the DSL.Thiskind
ofcross-domaincomputationshows the strength ofour domain-
agnosticapproach.
Results Most of the benchmarks used a single example while
the restusedno more than 3.TDS synthesizesall buttwo ofthe
benchmarksinunder10secondsandthe remainingtwoinunder
20seconds.
We also implemented the DSL and benchmarks in Sketch,
whichwasunabletosynthesizeanyofthemwithin10minutes.
6.1.4 Pex4Funprogramminggame
Motivation Althoughwebelieveourend-userprogrammingsce-
nariosarecompelling,wewantedtotestoursynthesizerinasce-
narioclosertotheTDDprogrammingstyleitwasinspiredbyand
getasourceforsomemorechallengingfunctionstosynthesize.To
thatend,wehadoursynthesizerplaythePex4Fun[32]program-
minggamewhereaplayerischallengedtoimplementanunknown
functiongivenonlya fewexamples.Eachtimetheplayerthinks
theyhaveasolution,thePex[31]testgenerationtoolusesdynamic
symbolicexecutiontocomparetheplayer’scodetoasecretrefer-
ence solution andgeneratesadistinguishinginputif the player’s
code does not match the specification.Pex provides the test for
the test stepoftheTDDwhile the playerisperforming the pro-
grammingstepwithoutfullknowledgeofthespecificationtheyare
codingfor.Thisisamore“pure”formofTDDastheplayerisnot
biasedintheircodingbyknowingthespecification,givingacloser
paralleltooursynthesizerwhichdoesnothaveknowledgeofthe
specificationofthefunctionitissynthesizing.
Experiment description Weuse a single DSL with aset of 40
simplestringandintfunctionswhichmaybecombinedinany
type-safewaytoshowthatwhileacarefullyconstructedDSLcan
begiventooursynthesizertomakeitperformespeciallywellina
givendomain,it can still successfullysynthesizeprogramsusing
aless specialized DSL capable of describing a wider range of
programs.Note that ourDSL waswrittenwithoutlookingat the
188
1
10
100
0
0.2
0.4
0.6
0.8
1
Normalized execution time
Normalized inversions count
Figure 7. Norm.time(1=opt)formanyreorderingsofexamples
(dist.measuredininversions,norma.so1=reverse);thelineshows
thegeo.meanofthedatapointsforeachnorm.inversioncount.
0
0.2
0.4
0.6
0.8
1
0
0.1
0.2
0.3
0.4
0.5
0.6
0.7
0.8
0.9
1
Proportion failed
Normalized inversions count
0
4
2
12
9
14
13
4
2
2
Figure 8. Prop. ofreorderingsTDS failedonbynorm.inversion
count.Numbersabovebarsareabsolute#offailedreorderings.
Pex4Funpuzzlesandthereforeendedupmissingsomefunctions
necessaryforsomepuzzleslikebitwiseoperations.
ForeachpuzzleinthePex4Fundata,wehadouralgorithmplay
Pex4Funforamaximumof7iterations,afterwhichthesynthesizer
wasconsideredtohavefailedifitstillhadnotproducedasolution.
Thismayseemliketoofewiterations,butit ismorecallstoPex
thanmostusersusedforanyofthepuzzles.
Forsomeofthepuzzles,usingPextogeneratetestcasesfailed
togenerate asolutiondespitemanualinspectiondeterminingthat
thepuzzleswerewellwithinthecapabilitiesofthesynthesizerand
theDSLused.Insuchcases,asequenceoftestcaseswasgenerated
manuallytosynthesizesolutionstothosepuzzles.
Benchmarks The puzzles our synthesizer could synthesize in-
cluded,amongmanyothers,factorial,swappingelementsofanar-
ray,andsummingnumbersinastringdelimitedbydelimiterspec-
ifiedonthefirstlineofthestringandsomemoretrivialexamples
likeconcatenatingthefirstandlastelementofastringarray.
The remainingunsynthesizedpuzzleseither involvedlooping
structuresnot covered by our strategies (e.g., count the number
ofstepsofthe3n+1 problem
2
neededtoreach1),components
notinourcomponentset (e.g.computebitwise or),orarithmetic
expressionstoolargetoconstructusingcomponent-basedsynthesis
(e.g.computethevalueofaspecificcubicpolynomial).
Results We ran our experiment across 172 randomly selected
puzzlesfromPex4Fun.The synthesizerfoundsolutionsfor72of
those.For60ofthose,thetestcasesgeneratedbyPexweresuffi-
cient,butforanother12thetestcaseshadtobewrittenmanually.
6.2 Exampleordering
WehypothesizedthatexampleorderingisusefulandTDSisrobust
tosmallvariationsinexampleorder.Forthe vast majorityofour
benchmarks,the number ofexamples issmall and their order is
unimportant;theuseofcontextsandsubexpressionsfromthepre-
viousprogramisimportant(whennotsynthesizingfromasingle
2
https://en.wikipedia.org/wiki/Collatz_conjecture
0
10
20
30
40
50
F
la
s h
F
ill
T
a b
le
s
X
M
L
P
e
x 4 F
u
n
M
a n
u a
l
P
e x 4
F
u
n P
e x
# synthesized
Benchmark set
full
no contexts from prev.
no subexprs from prev.
nothing from prev.
no DSL
Figure9. #synthesizedbybenchmarksetandfeaturesenabledin
algorithm.“full”isthefullalgorithm,contextsandsubexpressions
frompreviousprogramtogetherformtheinformationTDSuses.
0.4
0.5
0.6
0.7
0.8
0.9
1
0
60
120
180
0.4
0.5
0.6
0.7
0.8
0.9
1
Proportion
Time (seconds)
Figure10. ExecutiontimesofallDBSruns.
example)asisshownin§6.3by disablingthem,butthe specific
orderofthe examplesisnot.Onthe otherhand,the12Pex4Fun
puzzleswhichrequiredmanuallywrittenexamplesequenceswere
difficultenoughforTDSthattheorderingofexampleswasinfact
valuabletothealgorithm.Togiveanideaofhowimportanttheor-
deringactuallywas,weranTDSonrandomlyreorderedcopiesof
thoseexamplesequences.
Fig. 7 shows the timing results for the example sequences
that were successfully synthesized. Each circle is one example
sequence,andthelineshowsgeometricmeanofcircles.
Thex-coordinatemeasureshowfarfromtheoptimalexample
sequenceitwaswhere0istheoptimalsequenceand1isthereverse
ofthe optimal sequence. Specifically, the value isthe number of
inversions
3
betweenthetwosequencesdividedbythe maximum
possiblenumberofinversions(
n(n 1)
2
forasequenceoflengthn).
They-coordinateisthetimeittooktosynthesizethesolutionusing
the random sequence measured in the time it took to synthesize
usingtheoptimalsequence.Notethatthey-axisisalogscale.
Fig. 8 shows for how many of the reorderings the program
wasnot successfully synthesized. The x-axis is the same; each
bar corresponds to a range of normalized inversion counts. The
barheightsare theproportionofsequencesforwhicha program
couldnotbesynthesized,andthenumbersabovethebarsarethe
absolutecounts.Therearemoreexamplestowardthemiddleasthe
sequenceswereselecteduniformlyatrandom,andtherearemore
possiblesequencesinthemiddle.
ThechartsshowtwoimportantpropertiesofTDS.First,itdoes
infactdependonexampleordering:largechangestotheexample
orderingmakeittakemuchlongertofindasolutionorfailtofind
asolution at all. Second, it is robust to small changes in the
exampleordering:fornormalizedinversioncountslessthan0.3,
fewerthanhalfthereorderingsfailedandthosethatsucceededtook
onaveragelessthanthreetimesaslongastheoptimalordering.
Those12examplesshowtheworstcaseforoursynthesizer.For
theother60Pex4FunpuzzleswithtestcasessequencesfromPex,
3
#ofexamplepairsthathavedifferentorderinthetwolists
124
51ofthemwerealsosuccessfullysynthesizedwiththosetestcases
inreverseorder.Forthe restoftheexamples,nearlyallcouldbe
synthesizedwiththeexamplessequenceinreverseorder,atworst
sloweddown bya factorof 3. Thisindicatesthat the sensitivity
totestcaseorderingisaffectedbyhowcomplicatedtheprogram
beingsynthesizedis.
6.3 Significanceofvariouspartsofalgorithm
In order to evaluate the usefulness of the different parts of our
algorithm,weranourbenchmarkswithpartsofitdisabled.Fig.9
showshowmanyofthebenchmarksweresynthesizedundereach
limitedversionofthealgorithm.
Iterativesynthesis Theiterative synthesisstrategyemployedby
TDSisimplementedbypassingcontextsandsubexpressionsfrom
thepreviousprogramtoDBS.Wedisabledthesetwopiecesofinfor-
mationindividuallyandtogether.ThePex4Funandtabletransfor-
mationbenchmarksweremostaffectedbytheremovaloffeatures
from TDS duetoworkingwith larger programs.Notably,we see
thateither thesubexpressionsorcontextsaloneishelpful,but
whencombinedtheyaresignificantlymorepowerful.
DSL-basedsynthesis WealsodisabledtheuseoftheDSLwhen
generatingcomponentsinDBS,soitinsteadwouldbelimitedonly
bythetypesofexpressions.There are no“no DSL” barsforthe
Pex4FunbenchmarksbecausethePex4FunDSLalreadyonlyused
thetypes,sothatconfigurationisidenticaltothe“full”configura-
tion.Manyoftheotherprogramsweresynthesizedfromjustasin-
gleexample,sotheweakeningofTDSdidnothavealargeeffect,
butthissuccesswasachieveddue tothe powerDBS gained from
theDSLascanbeseenfromthefactthatveryfewoftheend-user
benchmarkscouldbesynthesizedwithoutaccesstotheDSL.
6.4 Performance
Fig.10showsaCDFofallexecutiontimesofalloftheDBSruns
usedinourexperiments.Thischartshowsthat
isquiteeffi-
cientwithamedianrunningtimeofapproximately2seconds
andrunninginunder10secondsaround75%ofthetime.
Timeout Throughouttheexperiments,weuseda3minutetime-
out.OnlyveryrarelyinourexperimentsdidDBSeverrunforany-
wherenear3minuteswithouttimingout.Thereisavisiblebump
around60–70secondsafterwhichthelineisalmostflat,indicating
thatitisveryunlikelythatgivingDBSasmallamountofadditional
timewouldhavemadeanynoticeabledifferenceinourresults.This
isfurtherverifiedbyad-hocexperiencethatwithoutatimeout,DBS
runsforover30minuteswithoutaresultorrunsoutofmemory.
7. RelatedWork
Programmingbyexample Programmingbyexample(PBE)[7],
orinductive programming[16], isa subfieldof program synthe-
siscoveringmanydifferenttechniqueswhereaprogramisincom-
pletelyspecifiedbyexamples(inputspairedwithexplicitoutputsor
aqualityfunctionforresults).Inallofthepriorwork,alloftheex-
amplesaregivenatonce,althoughmuchofitusessomevariantof
geneticprogramming[23]whereprogramsarebuiltanditeratively
mutatedtowardasolutionorCEGIS[30]wherenewprogramsare
constructeduntilasolverfailstoprovideacounterexample,similar
tohowoursynthesizerwasusedwithPexinthePex4Funexperi-
ment.Akeyideainthe recentprior workisreducingthesearch
spaceusingversionspacealgebras[6,8,11,18,28,29],whichwe
avoidinordertomaintaingeneralityastheymustbe constructed
foragivendomain.
TDSismostsimilartopriorworkoncomponent-basedsynthesis
andgeneticprogramming.
Component-based synthesis Component-based synthesis is a
family oftechniquesthat perform program synthesisby starting
withasetof“components”—thatis,expressionsandfunctions—
andconsideringactualprogramsconstructedfromcombiningthese
components (as opposed to the version space algebra approach
wheretheactualprogramismerelyanartifactthatcanberecov-
eredafterthemainsynthesisalgorithmiscomplete).Component-
based synthesis has been successfully applied to a wide variety
ofdomainsincludingbit-vectoralgorithms[9],stringtransforma-
tions [24], peephole optimizations [5], type convertors [21, 27],
deobfuscation[13],andgeometryconstructions[10].
The actual search isperformed in different ways dictated by
the information required be known about the components. For
example, Gulwani et al. [9] used an SMT solver because their
componentsarestandardbitwisearithmeticoperators,sotheyhave
easilyexpressiblelogicalspecifications.Also,thisisthepriorwork
we found with the largest program synthesized by component-
basedsynthesisat16linesofcode,whichtookaroundanhourto
synthesize.Incomparison,ouralgorithmcansynthesizeprograms
ofupto20linesofcodewithin400secondsconsistingofarbitrary
user-definedfunctions.
ThepriorworkmostsimilartoourDBSisbyKatayama [15].
Likeouralgorithm,anyfunctioncanbeacomponentanditmain-
tainsanexplicitlistofthe componentsgeneratedsofaranduses
them whengeneratingcomponentson the nextstep.It findsand
prunesredundantcomponentsbyevaluatingeverycomponentona
subsetoftheexamplesandonlykeepingcomponentsthatevaluate
todifferentvaluesonsomeexample.Thisissimilartothepruning
donebyDBSexceptthatDBSusesallexamplesseensofar.
Genetic programming Genetic programming [23] synthesizes
programs by performing a genetic search which involves using
previouscandidateprogramstoproducenewcandidateprograms.
The primary difference between our work and genetic program-
mingisthatgeneticprogrammingisdirectedbyaqualityfunction
thattellshowwellagivenprogramperformsatthedesiredtaskand
reliesonthatqualityfunctionbeingwell-behavedwhileoursearch
isonlygivenabooleanfailureorsuccessoneachtestcase.
ADATE [25] takes as input a set of test inputs and quality
functionsfor theiroutputsand performs a genetic searchwhere
programsaremutatedandonlyprogramsthatimproveormaintain
thesumofthequalityfunctionvaluesarekept.Thisformulation
meansthatADATEhastochoosewhichtestcasetoimprovenext,
unlikeinoursystemwherethefirstktest casesmustpassbefore
thesynthesizerconsiderstestcasek+1.
Template-based synthesis Program sketching [30] is a form of
program synthesiswhere the programmer writesa sketch, i.e.,a
partialprogramwithholes,andprovidesaspecificationthesolution
mustsatisfy.LaSycanbeseenasalessprecisesketchwithaDSL
insteadofpartialbodies:infact,weportedourLaSyprogramsto
Sketchinordertodoacomparisonforourevaluation.However,the
searchstrategyisverydifferent:oursynthesizerfillsintheholes
usingcomponent-basedsynthesis(asopposedtousingSAT/SMT
solvers) and checks against input/output examples (instead of a
morecompletespecification).
Syntax-guidedsynthesis OurDSL-basedapproachissimilarto
thesyntax-guidedsynthesisideaproposedin[2],butismoreflexi-
blebyallowingforaDSLthatusesarbitrary.NETfunctions.That
work[2] onlypresentssimple prototypesynthesizerswhich lack
thepowerofTDS.SyGuS’suseofconstraintsinsteadofexamples
makesadirectcomparisonofsynthesizertechnologiesdifficult.
Rosette [33] isanextensiontothe Racket programming lan-
guagewhichallowseasyaccesstoasolverforapplicationsinclud-
ingsynthesisoverDSLsembeddedinRacket.Whiletheprogram-
merexperienceismuchsleekerthanwithSyGuSorLaSy,thesyn-
Documents you may be interested
Documents you may be interested
