A tool and case study for specification-based program review

Effective tool support is crucial for successfully applying software review techniques in practice. In this paper, we describe the design and implementation of a software tool to support an approach to reviewing programs on the basis of their formal specifications. The approach was initially proposed in our previous publication to improve the rigor, repeatability, and effectiveness of existing code review methods. We also present a case study in which we reviewed an ATM system to assess the performance of the review approach when used with the software tool. The results of the case study show that the approach is effective in detecting errors in programs and the tool is helpful in enhancing the efficiency of the review process.