A review approach to detecting structural consistency violations in programs

The application of specification-based program verification techniques (e.g., testing, review, and proof) usually faces strong challenges in practice when the gap between the structure of a specification and that of its program is large. In this paper we describe an approach to detecting the violations of the structural consistency in programs based on their specifications by review. The approach is aimed at supporting software development in which programs are constructed based on their formal specifications. We establish a set of criteria and a review process that can guide reviewers to uncover structural consistency violations in programs, and apply the approach in a case study to assess its effectiveness.