Evaluating formal specifications : a cognitive approach

Abstract

This thesis explores a new approach for supporting software engineering claims with empirical evidence and investigates whether the human potential for error when reasoning about formal specifications can be reduced. The cognitive science literature has shown that people succumb to various forms of systematic error and bias when reasoning about natural language statements containing logical connectives. A series of empirical studies are reported, which use the framework of the Z notation to test whether people are liable to commit the same errors and biases when reasoning about formal specifications. The results suggest that the ways in which people reason about formal expressions are influenced by grammatical properties of the specification, such as the degree of thematic content or the polarity of logical terms, and by attributes of the reasoned, such as length of experience or degree of expertise. The empirical data is then recast into a tentative predictive model for quantifying how far properties of formal specifications are likely to evoke erroneous inferences. The model may be used as an empirical basis for assessing some of the claims associated with formal methods, or as a basis for engineering formal specifications with less propensity for eliciting erroneous development decisions.