Specification is the process of translating a problem into a formal description. This should be kept in mind even if we tend to use this term only for the final result of the process. Indeed, it is a characteristic of Western culture that it puts less emphasis on the process than on the form it creates (see Bohm; Whorf). Following Gregory Bateson, development always alternates between process and form. When the process of specification comes up with axioms defining the problem, we start the process of computation, for instance, deriving theorems. These are expected to improve our understanding of the problem so as to get closer to a solution. But theorems may also reveal flaws in our reasoning, hidden assumptions or undesired effects. In such a case we modify the specification and enter a new cycle of producing forms and initiating processes. Specification and theorem-proving tools should support this activity. However, they should not be designed with the intention of relieving us of the whole work. Many decisions are involved for which there is no proper reason to transfer them to a formal system or a machine. We think it necessary to stress this point because computer scientists sometimes ignore the limits of formal methods. Apart from ethical questions, there is no evidence at all that the heart of formal reasoning, namely deduction, plays a significant role in the problem-solving activity of our minds (Dreyfus and Dreyfus; Searle). Formal methods do not stand in their own right. They live with the people who use them (see Naur [1,2]).
KeywordsFormal Method Horn Clause Automate Theorem Prove Bibliographic Note Abstract Data Type
Unable to display preview. Download preview PDF.