17 feb. 1999
3 minuten
Al sinds zijn studententijd werkt Armando Solar-Lezama, nu professor in MIT’s Department of Electrical Engineering and Computer Science, aan een programmeertaal die het voor prohrammeurs mogelijk maakt om eenvoudigweg sommige details uit hun code weg te laten. De programmeertaal, Sketch genaamd, vult dan zelf de leemtes in.
Als het helemaal is uitontwikkeld, en gebruiksvriendelijker gemaakt, kan Sketch uiteindelijk het leven vande software-ontwikkelaar een stuk aangenamer maken. Maar in de tussentijd kan het zijn waarde bewijzen als basis voor andere tools die het mechanisme van ‘programmasynthese’ of automatische programmageneratie benutten.
Tijdens de afgelopen Verification, Model Checking, and Abstract Interpretation Conference beschreven Solar-Lezama en een aantal van zijn studenten een nieuwe uitbreiding van Sketch, die het in veel gevallen mogelijk maken om complexe synthese-taken veel efficiënter uit te voeren. De onderzoekers testten die nieuwe versie van Sketch op diverse al bestaande applicaties. Waar de voorgaande versie in sommige gevallen een ‘time out’ gaf, of zo lang zou doen over het bereiken van een oplossing dat hij het opgaf, kon de nieuwe versie de code van de studenten in enkele milliseconden corrigeren.
Sketch behandelt programmasynthese als een zoekprobleem. Het evalueert een enorm scala aan mogelijke variaties op hetzelfde basisprogramma tot het er een vindt die voldoet aan de criteria van de programmeur. Als het onderzochte programma te complex is, wordt de zoekruimte ‘opgeblazen’ tot een onbetaalbaar groot formaat. In hun nieuwe paper beschrijven de onderzoekers hoe die zoekruimte kan worden ingekrompen.
‘Chain of command’
"Als je via synthese een groter stuk code probeert te maken, moet je vertrouwen op andere functies, andere sub-delen van de code", legt student Rishabh Singh uit. "Als in voorkomende gevallen het systeem alleen afhankelijk is van bepaalde eigenschappen van de sub-delen, zou je dat op een of andere manier moeten kunnen uitdrukken in een high-level taal. Als het je lukt om te specificeren dat slechts bepaalde eigenschappen zijn vereist, ben je in staat om via synthese met succes een langere code te genereren."
Ter illustratie geeft Singh een voorbeeld waarbij een van de subdelen van de code een routine is voor het vinden van de wortel van een getal, en waarbij een functie op hoger niveau afhankelijk is van het resultaat van die berekening. Als de eerdere versie van Sketch probeerde variaties van die high-level functie te evalueren, moest hij voor elke variatie ook de variaties van de wortelfunctie evalueren. Omdat woreltrekken een complex proces is zou dat zoeken tijdrovend en kostbaar worden.
Met de nieuwe versie kan de programmeur echter eenvoudig de voorwaarden specificeren waaraan de wortel-functie moet voldoen. De output vermenigvuldigd met zichzelf moet gelijk zijn aan de input. Nu kan Sketch er genoegen mee nemen dat de voorgestelde wortelfunctie voldoet aan de criteria, en verder gaan naar de high-leverl functie. Het hoeft niet meer voor elke variatie de wortelfunctie te evalueren.
In feite legt dit een iets grotere verantwoordelijkheid bij de programmeur, die nu moet beredeneren aan welke criteria elke low-level functie moet voldoen. Maar het stelt Sketch in staat om veel complexere problemen te behandelen.
Expertise nodig
Solar-Lezama benadrukt dat er nog veel werk moet worden verricht voordat Sketch bruikbaar is voor commerciële software-ontwikkelaars. "Maar we heben overtuigend bewezen dat het al goed gebruikt kan worden bij het bouwen van tools, door verschilende systemen te bouwen die dingen kunnen doen die eerder niet mogelijk waren."
Hij onderzocht de bruikbaarheid van Sketch bij beginnende studenten met slecht één semester programeerervaring. In alle gevallen maakten de studenten met succes gebruik van Sketch om werkende code te produceren. Maar ook bleek dikwijls dat de synthese van ontbrekende code onacceptabel lang duurde, als gevolg van de manier waarop de studenten het probleem hadden beschreven.
"Er is nog een bepaald niveau van expertise en begrip van de onderliggende technologie nodig, om te voorkomen dat het explodeert", zegt Solar-Lezama. "Voor ons ambitieuze doel dat iederen C terzijde schuift en overstapt op Sketch moeten we nog wel wat werk verzetten".
