Measuring human inferential complexity in formal specifications : a predictive model for the Z notation

The entire history of software engineering informs us that failure to interpret or reason correctly with software specifications causes developers to make incorrect development decisions which can lead to the introduction of faults or anomalies in software systems. Most key development decisions are usually made at the early system specification stage of a software project and developers do not receive feedback on their accuracy until near its completion. Software metrics are generally aimed at the coding or testing stages of development, however, when the repercussions of erroneous work have already been incurred. This paper presents a tentative model for predicting those parts of formal specifications which are most likely to admit erroneous inferences, in order that potential sources of human error may be reduced. The empirical data populating the model was generated during a series of cognitive experiments aimed at identifying linguistic properties of the Z notation which are prone to admit non-logical reasoning errors and biases in trained users.