Detail of a work
Y. Muto, "Variable Coverage: a Metric to Evaluate the Exhaustiveness for Program Specifications Based on Dbc," Master thesis, Osaka University, 2012.
ID 181
分類 学位論文
タグ verification formal methods quality metrics
表題 (title) Variable Coverage: a Metric to Evaluate the Exhaustiveness for Program Specifications Based on Dbc
表題 (英文)
著者名 (author) Yuko Muto
英文著者名 (author) Yuko Muto
キー (key) Yuko Muto
学校名 (school) Osaka University
出版社住所 (address)
刊行月 (month) 2
出版年 (year) 2012
URL
付加情報 (note)
注釈 (annote)
内容梗概 (abstract) 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.
論文電子ファイル 利用できません．
BiBTeXエントリ 
@masterthesis{id181,
         title = {Variable Coverage: A Metric to Evaluate the Exhaustiveness for Program Specifications Based on DbC},
        author = {Yuko Muto},
        school = {Osaka University},
         month = {2},
          year = {2012},
}