Static Detection of Implementation Errors Using Formal Code Specification

The software engineering community suggests that formal specification of source code facilitates the verification that can help to identify hidden functional errors. In this work, we investigate the impact of various levels of formal specification on the ability to statically detect errors in code. Our goal is to quantify the return on investment with regards to the effectiveness of identifying errors versus the overhead of specifying software at various levels of detail. We looked at common algorithms and data structures implemented using C# and specified using Spec#. We selectively omitted various parts of the specification to come up with five different levels of specification, from unspecified to highly-specified. For each level of specification, we injected errors into the classes using a fault injection tool. Experimentation using a verifier showed that over 80% of the errors were detected from the highest specification levels while the levels in between generated mixed results. To the best of our knowledge, our study is the first to quantitatively measure the effect of formal methods on code quality. We believe that our work can help convince skeptics that formal methods can be practically integrated into programming activities to produce code with higher quality even with partial specification.