Seven lesser known myths of formal methods : uncovering the psychology of formal specification

Abstract

Psychological research has shown that people are prone to systematic errors when reasoning about logical statements in natural language. The Human Cognition and Formal Methods research project aims to test whether people are equally susceptible to error when reasoning about the same types of logical statement in formal notations. A series of specially designed experiments plan to investigate specific properties of formal notations that could affect the ease with which people are able to understand and reason about formal specifications. The first experiment concentrated on five cognitive activities which are central to the process of developing a formal specification: reading, writing, understanding, translating and reasoning. It also examined the ways in which a designer's writing style can affect his or her audience's understanding of a specification. The results of the experiment suggested that some of the software engineering community's widely held beliefs about formal methods might, in fact, be misconceptions. This paper uncovers seven such "myths" based on the experiment's findings and discusses their possible implications for the future practice of software specification.