Reasoning about formal software specifications : an initial investigation

Within the software engineering community, it is widely believed that formal logic based notations could hold the key to overcoming some of the classical problems associated with program specification. Over the past three decades, psychology has investigated the difficulties that people experience when reasoning about logical statements in natural language. The Human Cognition and Formal Methods project aims to test whether these studies' findings carry over into the domain of formal specification by conducting a series of specially designed experiments. The first experiment concentrated on five cognitive activities central to formal specification: reading, writing, understanding, translating and reasoning. It also investigated the ways in which designers' personalities affect their specifications and their audience's interpretations of them. Its results are significant from a psychological perspective because they suggests that many of the erroneous inferences that people make about implicit logic in natural language also occur when reasoning about explicit logic in formal specifications. Its results are also significant from a computer science perspective because they appear to contradict several popular software engineering beliefs. This paper reports these results and points to similar findings obtained from previous psychological studies.