Experimental comparison of the comprehensibility of a Z specification and its implementation in Java

Snook, C. F. and Harrison, R. (2004) Experimental comparison of the comprehensibility of a Z specification and its implementation in Java. Information and Software Technology, 46 (14). pp. 955-971. ISSN 0950-5849 doi: 10.1016/j.infsof.2004.04.003

Abstract/Summary

Comprehensibility is often raised as a problem with formal notations, yet formal methods practitioners dispute this. In a survey, one interviewee said 'formal specifications are no more difficult to understand than code'. Measurement of comprehension is necessarily comparative and a useful comparison for a specification is against its implementation. Practitioners have an intuitive feel for the comprehension of code. A quantified comparison will transfer this feeling to formal specifications. We performed an experiment to compare the comprehension of a Z specification with that of its implementation in Java. The results indicate there is little difference in comprehensibility between the two. (C) 2004 Elsevier B.V. All rights reserved.