Collaborative Research: SHF: Small: Verification-guided Assessment and Reduction of Code Complexity

Software developers spend much of their time reading and understanding (“comprehending”) code, because it is a prerequisite for adding new features, correcting defects, improving existing functionality, and performing other changes to software systems. Prior research has proposed many syntactic metrics that claim to measure code complexity, but the correlation between these metrics and measurements of code comprehension effort from humans is weak, at best. Developers still have limited support for assessing and reducing the complexity of their code to decrease code comprehension effort. This project will investigate new semantic metrics of code complexity derived from existing automated reasoning tools (“verification tools”). These new metrics will be semantic (i.e., based on the program’s meaning) rather than syntactic (i.e., based on the program’s textual representation). If these new, semantics-based metrics correlate better than prior syntactic metrics with human comprehension effort, they will help guide software developers to write code that is easier to understand and modify, thereby improving software quality and reducing software development costs.The key insight that inspires this project is that the output of verification tools contains useful information about a program’s semantic complexity. Verification tools try to prove that a program does or does not have a particular property, such as “cannot dereference a null pointer” or “eventually halts." Because these kinds of semantic program properties are undecidable, verification tools are always approximate: they conservatively answer “I don’t know” when they cannot construct a proof. Such “I don’t know” answers from verification tools may be a useful source of information about a program’s semantic complexity, and a preliminary study found a correlation between such “I don’t know” answers and human comprehension effort. Intuitively, the fewer facts that a suite of verification tools can prove about a program, the more complex that program probably is. This project will investigate three research directions based on this insight: (1) validate the hypothesis that the success or failure of verification (i.e., verifiability) is correlated with code complexity and human-based code comprehension effort (i.e., comprehensibility), and establish whether a causal relationship exists between verifiability and comprehensibility or whether they have some mutual cause; (2) use the semantic code information encoded in the output of verifiers to improve the performance of existing predictive models of comprehensibility that currently rely on syntactic features only; and (3) “verifier-guided” code refactoring to reduce complexity and comprehensibility in an automated way, using information about the parts of programs that verifiers struggle with as a guide for where and how to apply refactorings.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.