概要: Along with increasing the size of software, formal methods have played an important role. Design by Contract is a notion for program languages by formal methods, using constraints as contracts between the caller and the callee routines. Some verifiers are able to check whether given source code and constraint meet or not. However, it is hard to measure the exhaustiveness for specification, that is, how much constraints cover ideal specification for source code. If a verifier checks source code with no constraints, the result would be valid regardless of the quality of source code because of emptiness of specification. Although some verification coverages have been proposed for hardware such as HDL and FSM, there are a few coverages to measure the exhaustiveness of specification for source code, for general purpose programing languages at the implementation level. In this paper, we propose Variable Coverage, a simple metric to check the exhaustiveness of specification with source code for Java and other Object-Oriented programming languages. Our proposed coverage observes occurrence of variables in constraints (i.e., specification), such that the variables are used in the target method/constructor. We applied our approach to three programs in order to evaluate that Variable Coverage is able to help to find variables which should have been referred in specifications as important variables. As a result, we found some shortage of JML annotations in target programs, which shows the usefulness of our proposed metric. タグ: verification, formal, methods, quality, metrics

@mastersthesis{YukoMuto2012,
  author = {Yuko Muto},
  title = {Variable Coverage: A Metric to Evaluate the Exhaustiveness for Program Specifications Based on DbC},
  school = {大阪大学},
  year = {2012},
  month = {feb}
}