Formal Systems

Part of the Texts in Computer Science book series (TCS)


Scientific experiments are of two kinds: (i) processes undertaken to discover things not yet known, (E1); and, (ii) processes undertaken to demonstrate things that are known, (E2). Scientific properties that have been observed will hold whenever the experiments are repeated with the same specifications, and under the same conditions. The results are independent of the scale on which the experiments are performed. Demonstrating the properties of a software system is analogous to conducting experiments of type E2. This can be done on a small scale, while establishing the properties of the software system through experiments on a reduced model of the system. However, the software development process is analogous to conducting experiments of type E1. This cannot be done on a small scale, or by employing a reduced model of the system. It is almost impossible to establish all the properties of a software system through the reduced model. It is therefore essential that software engineers get a direct exposure of the full-scale development process. On the other hand, a direct exposure of the full-scale development process may not be sufficient to reveal hidden properties of the system. A mid-way alternative is to adopt a certain degree of formality in software development. The motivation to espouse formal systems is driven by the quest for a foundation that is theoretically sound. A framework grounded on this foundation would contain the size and structural complexity of the system, provide a precise and unequivocal notation for specifying software components, and support a rigorous analysis of the relevant system properties. These observations are confirmed by the successful integration of formal methods in the development of large complex systems (Wheeler in, 2006; Formal Methods Web page, 2010).


Formal System Inference Rule Formal Language Deductive System Axiom System 


  1. 1.
    Backus JW (1957) The FORTRAN automatic coding system. In: Proceedings of the AFIPS Western joint computer conference, pp 188–198 Google Scholar
  2. 2.
    Bok C (2006) Developing an idea processor in prolog. Presented at the VIP-ALC Conference.
  3. 3.
    Formal Methods Web page,, May 2010
  4. 4.
    Johnson SC (1975) Yacc: yet another compiler. Computer science technical report No 32, Bell Labs, Murray Hill, NJ Google Scholar
  5. 5.
    Henderson P (1986) Functional programming, formal specification, and rapid prototyping. IEEE Trans Softw Eng SE-12(2):241–250 CrossRefGoogle Scholar
  6. 6.
    Hershey W (1985) Idea processors. Byte 10(4) Google Scholar
  7. 7.
    Martin J (2003) Introduction to languages and the theory of computation, 3rd edn. McGraw-Hill, New York Google Scholar
  8. 8.
    Naur P (ed) (1963) Revised report on the algorithmic language Algol 60. Commun ACM 6(1):1–17 Google Scholar
  9. 9.
    Peano G (1967) The principles of arithmetic, presented by a new method. In: van Heijenoort J (ed) From Frege to Gödel: a sourcebook of mathematical logic. Harvard University Press, Cambridge Google Scholar
  10. 10.
    Reisner P (1981) Formal grammar and human factors design of an interactive graphics system. IEEE Trans Softw Eng SE-7(2):229–240 CrossRefGoogle Scholar
  11. 11.
    Scowen RS (1998) Extended BNF—a generic base standard. Draft paper. (May 2010)
  12. 12.
    Wheeler DA (2006) High assurance (for security or safety) and Free-Libre/Open Source Software (FLOSS) … with lots on formal methods/software verification. (04/16/2010)

Copyright information

© Springer-Verlag London Limited 2011

Authors and Affiliations

  1. 1.Dept. Computer Science and Software Eng.Concordia UniversityMontrealCanada
  2. 2.Computer Science DepartmentUniversity of Wisconsin-La CrosseLa CrosseUSA

Personalised recommendations