Systeem dat automatisch de hiaten in programmeercode opvult is verbeterd

Systeem dat automatisch de hiaten in programmeercode opvult is verbeterd

Anonim

door Larry Hardesty, Massachusetts Institute of Technology

Image

Sinds hij afgestudeerd is, werkt Armando Solar-Lezama, universitair hoofddocent aan de afdeling Elektrotechniek en Computerwetenschappen van het MIT, aan een programmeertaal genaamd Sketch, waarmee programmeurs eenvoudigweg enkele computergegevens van hun code kunnen weglaten. Sketch vult dan automatisch de gaten in.

Als het wordt uitgewerkt en gebruiksvriendelijker wordt gemaakt, kan Sketch het leven van softwareontwikkelaars uiteindelijk gemakkelijker maken. Maar in de tussentijd bewijst het zijn waarde als de basis voor andere tools die gebruikmaken van de mechanica van 'programmasynthese' of het automatisch genereren van programma's. Recente projecten bij MIT's Computer Science and Artificial Intelligence Laboratory die op Sketch zijn gebouwd, omvatten een systeem voor het automatisch sorteren van programmeeropdrachten voor informatica-klassen, een systeem dat handgetekende diagrammen omzet in code en een systeem dat SQL-databasequery's produceert op basis van geschreven code op Java.

Op de Verification, Model Checking en Abstract Interpretation Conference van dit jaar beschreven Solar-Lezama en een groep van zijn studenten - grad studenten Rohit Singh, Rishabh Singh en Zhilei Zu, samen met MIT senior Rebecca Krosnick - een nieuwe uitwerking op Sketch die, stelt het in veel gevallen in staat om complexe synthesetaken veel efficiënter uit te voeren. De onderzoekers testten de nieuwe versie van Sketch op verschillende bestaande applicaties, waaronder het geautomatiseerde beoordelingssysteem. In gevallen waarin de vorige versie "een time-out" zou geven of zo lang zou duren om tot een oplossing te komen die het gewoon opgaf, kon de nieuwe versie de studentencode in milliseconden corrigeren.

Sketch behandelt programmasynthese als een zoekprobleem. Het idee is om een ​​enorm scala aan mogelijke variaties op hetzelfde basisprogramma te evalueren en er een te vinden die voldoet aan de criteria die door de programmeur zijn opgegeven. Als het te evalueren programma te complex is, wordt de zoekruimte ballonnen van een te groot formaat. In hun nieuwe artikel vinden de onderzoekers een manier om die zoekruimte te verkleinen.

Commandostructuur

"Wanneer u probeert een groter stuk code te synthetiseren, vertrouwt u op andere functies, andere subonderdelen van de code, " legt Rishabh Singh uit. "Als het zo is dat uw systeem alleen afhankelijk is van bepaalde eigenschappen van de subonderdelen, moet u dat op de een of andere manier kunnen uitdrukken in een taal op hoog niveau. Zodra u kunt opgeven dat alleen bepaalde eigenschappen vereist zijn, kunt u om de grotere code succesvol te synthetiseren. "

Stel bijvoorbeeld dat Singh uitlegt dat een van de subdelen van de code een routine is voor het vinden van de vierkantswortel van een getal en dat een functie op een hoger niveau afhankelijk is van de resultaten van die berekening. Als de vorige versie van Sketch variaties van de functie op hoog niveau zou proberen te evalueren, zou het voor elke variatie ook variaties van de vierkantswortelfunctie moeten evalueren. Omdat het vinden van vierkantswortels een complex proces is, zou het zoeken onbetaalbaar tijdrovend zijn.

Met de nieuwe versie van Sketch kan de programmeur echter eenvoudig voorwaarden opgeven waaraan de vierkantswortelfunctie moet voldoen: de output vermenigvuldigd met zichzelf moet gelijk zijn aan de input. Nu kan Sketch zichzelf ervan overtuigen dat de vierkantswortelfunctie die het bedenkt, aan dat criterium voldoet en naar de functie op hoger niveau gaat. Het hoeft de vierkantswortelfunctie niet bij elke doorgang opnieuw te evalueren.

In feite legt dit een iets grotere verantwoordelijkheid op de programmeur, die nu moet redeneren over de criteria waaraan elke functie op laag niveau moet voldoen. Maar het stelt Sketch in staat om veel gecompliceerdere problemen aan te pakken.

Onmiddellijke vooruitzichten

Solar-Lezama geeft toe dat het heel wat werk zal vergen voordat Sketch nuttig is voor commerciële softwareontwikkelaars. "De applicatie als infrastructuur voor het bouwen van tools, en het gebruiken om daarbovenop systemen van een hoger niveau te bouwen, hebben we heel overtuigend aangetoond door een verscheidenheid aan systemen te bouwen die dingen doen die voorheen niet mogelijk waren", zegt hij.

Hij heeft echter bruikbaarheidstudies uitgevoerd met Sketch, waarbij MIT-studenten zijn aangenomen met slechts een semester aan programmeerervaring om het te testen. In alle gevallen, zegt hij, hebben de studenten Sketch met succes gebruikt om werkcode te produceren. Maar in veel gevallen duurde het onacceptabel lang om de ontbrekende code te synthetiseren, vanwege de manier waarop de studenten het probleem hadden beschreven.

"Het vereist nog steeds een niveau van expertise en begrip van de onderliggende technologie om niet op te blazen", zegt Solar-Lezama. "Wat betreft het ambitieuzere doel van iedereen om C te dumpen en in plaats daarvan Sketch te gebruiken, moeten we nog steeds behoorlijk pushen."

Zoals Rajeev Alur, professor aan de Afdeling Computer- en Informatiewetenschappen aan de Universiteit van Pennsylvania, uitlegt, baseert de nieuwe paper zich op principes uit het veld van "formele verificatie", die, zegt Alur, methoden onderzoekt voor "het controleren van de juistheid van programma's die geautomatiseerd redeneren gebruiken. "

"Bij verificatie hebben mensen altijd modulair redeneren gebruikt als een techniek om het op te schalen naar interessantere systemen", zegt Alur. "Wat dit artikel doet, is een aantal van die ideeën nemen en ze mooi combineren met de syntheseroutines die ze in Sketch hebben."

Alur erkent dat "het gebruik van een algemene softwareontwikkelaar [Sketch], misschien is dat niet realistisch binnen afzienbare tijd." Maar, zegt hij, "zelfs nu kan het worden gebruikt voor zeer specifieke, gespecialiseerde taken. Als je om een ​​of andere reden een stukje code probeert te optimaliseren, in plaats van al die aanpassingen handmatig te doen, nu een systeem zoals Sketch het zou kunnen doen. "