Automated generation of assert statements with Toradocu

Do you love writing test assertions?  If not, the Toradocu tool can help you.  Toradocu 1.0 has just been released.

Toradocu automatically generates assert statements that you can insert in your program.  This makes your existing tests more effective, and it can also find errors during normal operation of your program.

Toradocu converts your existing Javadoc comments into assertions.  It works as follows:

• It parses an English sentence, yielding a parse tree that indicates the subject, the verb, the direct and indirect objects, etc.
• It associates every noun phrase in the sentence with an expression in the program.  It does so by comparing the text of the noun phrase with variable names and types.
• It associates every verb in the sentence with an operation in the program.  For example, it compares the text of the verb with method names.
• Now that every noun and verb in the parse tree is associated with a program element, the sentence can be translated to a Java expression that can be used in an assert statement.

For example, suppose you wrote

 @throws IllegalArgumentException if the argument is not in the list and is not convertable

Toradocu aims to determine that "argument" refers to the method's formal parameter, "the list" refers to some variable whose type is a subtype of List, and "convertable" is determined by some method whose name or documentation refers to "convert".  Toradocu generates an aspect that you can weave into your program.  The aspect indicates an error whenever your program should throw IllegalArgumentException but does not, and the aspect indicates an error whenever your program should not throw an IllegalArgumentException but does so.  This helps you ensure that your program and its documentation are consistent.

Toradocu is described in greater detail in the ISSTA 2016 paper "Automatic generation of oracles for exceptional behaviors".

Toradocu 1.0 works only for @throws Javadoc tags, and achieves precision and recall around 70%.  We are working to improve the results, to add support for @param and @return tags, and to integrate Toradocu into test generators such as Randoop.

FSE 2016 student research competition

My students took 4 of the 6 awards in the FSE 2016 SRC (student research competition), including both first-place awards.

Undergraduate category:

1. "Combining bug detection and test case generation", Martin Kellogg, University of Washington
2. "Bounded model checking of state-space diginal systems", Felipe Monteiro, Federal University of Amazonas
3. "Preventing signedness errors in numerical computations in Java", Christopher Mackie, University of Washington

Graduate category:

1. "Cozy: Synthesizing collection data structures", Calvin Loncaric, University of Washington
2. "How should static analysis tools explain anomalies to developers?" Titus Barik, North Carolina State University
3. "Evaluation of fault localization techniques", Spencer Pearson, University of Washington

Congratulations to all the winners!

Here are more details about each of the UW projects.

"Combining bug detection and test case generation", by Martin Kellogg

Software developers often write tests or run bug-finding tools.  Automated tools for these activities sometimes waste developer time: bug finders produce false positives, and test generators may use incorrect oracles. We present a new technique that combines the two approaches to find interesting, untested behavior, in a way that reduces wasted effort. Our approach generates tests that are guaranteed to rule out ("kill") some mutant that could not be killed by the existing test suite.  The developer must only determine whether the program under test is behaving correctly. If it is, then the new test case—which improves mutation coverage—can be added to the test suite. If it is not behaving correctly, then our approach has discovered and reproduced a bug.  We demonstrated that the technique can find about a third of historical defects while only bothering the developer with truly novel input.

"Preventing signedness errors in numerical computations in Java", by Christopher Mackie

If a program mixes signed and unsigned values, it will produce meaningless results.  We have developed a verification tool that prevents such errors.  It is built on a type system that segregates signed from unsigned integers.  In a case study, our type system proved easy to use, and it detected a previously-unknown bug. Our type system is implemented as the Signedness Checker and is distributed with the Checker Framework.

"Cozy: Synthesizing collection data structures", by Calvin Loncaric

Many applications require specialized data structures not found in standard libraries. Implementing new data structures by hand is tedious and error-prone.  To alleviate this difficulty, we have built a tool called Cozy that synthesizes data structures using counter-example guided inductive synthesis. We have evaluated Cozy by showing how its synthesized implementations compare to handwritten implementations in terms of correctness and performance across four real-world programs. Cozy's data structures match the performance of the handwritten implementations while avoiding human error.

"Evaluation of fault localization techniques", by Spencer Pearson

Given failing tests, a fault localization tool attempts to identify which lines of source code are responsible for the failures. So far, evaluations of fault localization tools have overwhelmingly relied on artificial faults, generated by mutating correct programs.  Researchers have assumed that whichever tools best localize artificial faults will best localize real-world faults. We tested this by repeating several previous evaluations on both kinds of faults, and found that the assumption was false on our data set: artificial faults were not useful for identifying the best fault localization tools! Since this result calls into question all previous studies of these tools, we examined what makes a tool do well at localizing real faults, and we designed a new technique that outperforms all prior techniques we studied, on real faults.  Our technical report is available at http://www.cs.washington.edu/tr/2016/08/UW-CSE-16-08-03.pdf.

OOPSLA 2016 papers

OOPSLA 2016 was in Amsterdam this week.  Each day of the conference, one of my students presented his work:

On Wednesday, Pavel Panchekha presented "Automated Reasoning for Web Page Layout".  To create a good-looking HTML webpage, it is necessary to use CSS styling.  Pavel's Cassius system takes as input a picture or mockup of a webpage, and it outputs a CSS stylesheet that will produce the given layout.  This is one application of a formalization of CSS that can be used not just for synthesis of CSS code, but also for automated verification and debugging.

On Thursday, Konstantin Weitz presented "Scalable Verification of Border Gateway Protocol Configurations with an SMT Solver".  BGP is a networking protocol that determines how packets are routed through the internet.  ISPs configure their routers with BGP configurations, with the aim of providing good service, making a profit, satisfying contractual obligations, and not disrupting other parts of the Internet.  The Bagpipe tool verifies these properties, and it found multiple errors in real-world BGP configurations.

On Friday, Calvin Loncaric presented "A Practical Framework for Type Inference Error Explanation". Type inference is famous for being a powerful way to relieve programmers of the burden of writing types, and is equally famous for giving misleading error messages, often in the wrong part of the program, when the program contains an error.  Calvin's work shows a way to improve the error messages that are produced by type inference.

If you missed the conference, then be sure to check out their papers!