Summary
Describes technique (and tool, Tikanga) for computing operational preconditions: a description of how to satisfy a function’s preconditions (e.g. call createX to obtain an X, then you can pass that to consumeX). Process: create object usage models for identifiable objects; convert to prefix models that focus on call events; transform prefix models into Kripke structures; generate a set of CTL formulas using the Kripke structures; model check those and filter out any that do not hold; for each formal parameter of a method, look for sets of CTL formulas that are common to many objects passed to that method, these form an operational precondition. Violations of operational preconditions are then located, ranked and reported to the user as potential bugs. Evaluation provided on six extant Java projects.

Comments
This is definitely an interesting idea. In theory, you can figure out how the arguments to methods are generally “prepared” before a method is called. Since this includes the receiver, this encompasses something of the idea of type states as well. Then you can either use this information to provide usage examples or look for potentially bogus usage which might indicate bugs. However, its application to that latter task turned up an awful lot of false positives (spoken as a programmer, rather than a researcher; apparently 56% false positives is good compared to other research techniques). They didn’t characterize the types of bugs it found, and I’d be interested in seeing that. Are they subtle? Are they the sorts that are already found by already widely deployed techniques? I’m also curious about how difficult it is to wade through the false positives. Does one have to pore over a lot of source to tell whether the tool is pointing out something meaningful?

Source: SU