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. © 2013 Springer-Verlag.
CITATION STYLE
Saleh, I., Kulczycki, G., Blake, M. B., & Wei, Y. (2013). Static detection of implementation errors using formal code specification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8137 LNCS, pp. 197–211). https://doi.org/10.1007/978-3-642-40561-7_14
Mendeley helps you to discover research relevant for your work.