• Peter Padawitz
Part of the EATCS Monographs on Theoretical Computer Science book series (EATCS, volume 16)


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]).


Formal Method Horn Clause Automate Theorem Prove Bibliographic Note Abstract Data Type 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag Berlin Heidelberg 1988

Authors and Affiliations

  • Peter Padawitz
    • 1
  1. 1.Fakultät für Mathematik und InformatikUniversität PassauPassauGermany

Personalised recommendations