Featured Research

from universities, journals, and other organizations

System that automatically fills gaps in computer programmers' code gains power

Date:
February 25, 2014
Source:
Massachusetts Institute of Technology
Summary:
A system that automatically fills in the gaps in programmers' code becomes more powerful. A recent programming language called Sketch allows programmers to simply omit some of the computational details of their code. Sketch then automatically fills in the gaps.

Since he was a graduate student, Armando Solar-Lezama, an associate professor in MIT's Department of Electrical Engineering and Computer Science, has been working on a programming language called Sketch, which allows programmers to simply omit some of the computational details of their code. Sketch then automatically fills in the gaps.
Credit: Illustration: Christine Daniloff/MIT

Since he was a graduate student, Armando Solar-Lezama, an associate professor in MIT's Department of Electrical Engineering and Computer Science, has been working on a programming language called Sketch, which allows programmers to simply omit some of the computational details of their code. Sketch then automatically fills in the gaps.

Related Articles


If it's fleshed out and made more user-friendly, Sketch could ultimately make life easier for software developers. But in the meantime, it's proving its worth as the basis for other tools that exploit the mechanics of "program synthesis," or automatic program generation. Recent projects at MIT's Computer Science and Artificial Intelligence Laboratory that have built on Sketch include a system for automatically grading programming assignments for computer science classes, a system that converts hand-drawn diagrams into code, and a system that produces SQL database queries from code written in Java.

At this year's Verification, Model Checking, and Abstract Interpretation Conference, Solar-Lezama and a group of his students -- grad students Rohit Singh, Rishabh Singh, and Zhilei Zu, along with MIT senior Rebecca Krosnick -- described a new elaboration on Sketch that, in many cases, enables it to handle complex synthesis tasks much more efficiently. The researchers tested the new version of Sketch on several existing applications, including the automated grading system. In cases where the previous version would "time out," or take so long to reach a solution that it simply gave up, the new version was able to correct students' code in milliseconds.

Sketch treats program synthesis as a search problem. The idea is to evaluate a huge range of possible variations on the same basic program and find one that meets criteria specified by the programmer. If the program being evaluated is too complex, the search space balloons to a prohibitively large size. In their new paper, the researchers find a way to shrink that search space.

Chain of command

"When you're trying to synthesize a larger piece of code, you're relying on other functions, other subparts of the code," Rishabh Singh explains. "If it just so happens that your system only depends on certain properties of the subparts, you should be able to express that somehow in a high-level language. Once you are able to specify that only certain properties are required, then you are able to successfully synthesize the larger code."

For instance, Singh explains, suppose that one of the subparts of the code is a routine for finding the square root of a number, and a higher-level function relies on the results of that computation. If the previous version of Sketch were trying to evaluate variations of the high-level function, for each variation, it would also have to evaluate variations of the square-root function. Since finding square roots is a complex process, that would make the search prohibitively time-consuming.

With the new version of Sketch, however, the programmer can simply specify conditions that the square-root function has to meet: The output multiplied by itself must equal the input. Now, Sketch can satisfy itself that the square-root function it comes up with meets that criterion and move on to the higher-level function. It doesn't need to re-evaluate the square-root function at every pass.

In fact, this places a slightly greater onus on the programmer, who now has to reason about the criteria that each low-level function must meet. But it allows Sketch to handle much more complicated problems.

Immediate prospects

Solar-Lezama concedes that it will take a good deal of work before Sketch is useful to commercial software developers. "The application as a tool-building infrastructure, using it to build higher-level systems on top of it, we've demonstrated very convincingly by building a variety of systems that do things that couldn't be done before," he says.

He has, however, conducted usability studies with Sketch, recruiting MIT undergraduates with only a semester's worth of programming experience to test it. In all cases, he says, the students successfully used Sketch to produce working code. But in many cases, the missing code took an unacceptably long time to synthesize, because of the way the students had described the problem.

"It still requires a level of expertise and understanding about the underlying technology in order for it not to blow up," Solar-Lezama says. "As far as the more ambitious goal of everybody dumping C and using Sketch instead, we'd still have to push quite a bit."

Further information: http://people.csail.mit.edu/rishabh/papers/modelsVMCAI14.pdf


Story Source:

The above story is based on materials provided by Massachusetts Institute of Technology. The original article was written by Larry Hardesty. Note: Materials may be edited for content and length.


Cite This Page:

Massachusetts Institute of Technology. "System that automatically fills gaps in computer programmers' code gains power." ScienceDaily. ScienceDaily, 25 February 2014. <www.sciencedaily.com/releases/2014/02/140225101650.htm>.
Massachusetts Institute of Technology. (2014, February 25). System that automatically fills gaps in computer programmers' code gains power. ScienceDaily. Retrieved October 30, 2014 from www.sciencedaily.com/releases/2014/02/140225101650.htm
Massachusetts Institute of Technology. "System that automatically fills gaps in computer programmers' code gains power." ScienceDaily. www.sciencedaily.com/releases/2014/02/140225101650.htm (accessed October 30, 2014).

Share This



More Computers & Math News

Thursday, October 30, 2014

Featured Research

from universities, journals, and other organizations


Featured Videos

from AP, Reuters, AFP, and other news services

Mind-Controlled Prosthetic Arm Restores Amputee Dexterity

Mind-Controlled Prosthetic Arm Restores Amputee Dexterity

Reuters - Innovations Video Online (Oct. 29, 2014) A Swedish amputee who became the first person to ever receive a brain controlled prosthetic arm is able to manipulate and handle delicate objects with an unprecedented level of dexterity. The device is connected directly to his bone, nerves and muscles, giving him the ability to control it with his thoughts. Matthew Stock reports. Video provided by Reuters
Powered by NewsLook.com
Robots Get Funky on the Dance Floor

Robots Get Funky on the Dance Floor

AP (Oct. 29, 2014) Dancing, spinning and fighting robots are showing off their agility at "Robocomp" in Krakow. (Oct. 29) Video provided by AP
Powered by NewsLook.com
IBM Taps Into Twitter's Data With New Partnership

IBM Taps Into Twitter's Data With New Partnership

Newsy (Oct. 29, 2014) The new partnership will allow IBM to access Twitter’s data and analytics to help IBM clients better understand their consumers. Video provided by Newsy
Powered by NewsLook.com
Google To Use Nanoparticles, Wearables To Detect Disease

Google To Use Nanoparticles, Wearables To Detect Disease

Newsy (Oct. 29, 2014) Google X wants to improve modern medicine with nanoparticles and a wearable device. It's all an attempt to tackle disease detection and prevention. Video provided by Newsy
Powered by NewsLook.com

Search ScienceDaily

Number of stories in archives: 140,361

Find with keyword(s):
Enter a keyword or phrase to search ScienceDaily for related topics and research stories.

Save/Print:
Share:

Breaking News:

Strange & Offbeat Stories


Space & Time

Matter & Energy

Computers & Math

In Other News

... from NewsDaily.com

Science News

Health News

Environment News

Technology News



Save/Print:
Share:

Free Subscriptions


Get the latest science news with ScienceDaily's free email newsletters, updated daily and weekly. Or view hourly updated newsfeeds in your RSS reader:

Get Social & Mobile


Keep up to date with the latest news from ScienceDaily via social networks and mobile apps:

Have Feedback?


Tell us what you think of ScienceDaily -- we welcome both positive and negative comments. Have any problems using the site? Questions?
Mobile: iPhone Android Web
Follow: Facebook Twitter Google+
Subscribe: RSS Feeds Email Newsletters
Latest Headlines Health & Medicine Mind & Brain Space & Time Matter & Energy Computers & Math Plants & Animals Earth & Climate Fossils & Ruins