Verifier Warnings Do Not Improve Comprehensibility Prediction

TL;DR

This study investigates whether verifier warnings improve machine learning models' ability to predict code comprehensibility, finding that warnings do not significantly enhance performance.

Contribution

The paper empirically tests the utility of verifier warning counts as features in ML models for code comprehensibility prediction, showing limited benefit.

Findings

Verifier warning sum correlates with comprehensibility but offers limited predictive power.

Adding verifier warnings does not significantly improve ML model performance.

Syntactic and developer features alone are as effective as combined features including warnings.

Abstract

Proponents of software verification suggest that code simplicity is linked to the effort to verify code, hypothesizing that formal verifiers produce fewer false positive warnings and require less manual intervention when analyzing simpler code. A recent meta-analysis study found empirical support for this hypothesis: a small correlation between the sum of verifier warnings and human-derived code comprehensibility metrics. Based on this finding, we conjectured that using the sum of verifier tool (verifier) warnings to represent program semantic information as an input feature to machine learning (ML) models for code comprehensibility prediction can enhance their performance, when combined with traditional syntactic and developer features. To test this conjecture, we performed a control-treatment experiment incorporating the verifier warning sum feature into machine learning models from the literature, and conducted a comparative analysis of their performance against models trained only on syntactic and developer features. We found no significant difference in the prediction performance of models with and without the warnings feature. Our findings suggest that while a correlation exists, the verifier warning sum offers limited discriminative power: combining syntactic and developer features is just as effective for predicting human-judged code comprehensibility.