On the use of theory based systems to traverse educational gaps in computer system related activities

  • Peter E. Lauer
Part of the Lecture Notes in Computer Science book series (LNCS, volume 693)


Within the general setting of engineering trustworthy computer implementations of real-world systems, the paper delineates some of the gaps between theory and practice, and between system developers and users at various levels, and suggests how existing theory based systems could be used to help bridge these gaps more effectively than is the case at present.

Focus is on the gaps between conventional computer systems and theory based systems, and the gaps between knowledge and skill required for various levels of usage of the two types of system. Furthermore, identification of opportunities and tools supporting the transformation of systems and knowledge required to use them from the conventional to the theory based side will be of paramount interest.

Conventional Systems are considered to be based on doctrine, a rigorous body of knowledge and methods, for implementing real-world systems by computer systems.

Theory Based Systems are considered to be entirely based on theory, a formal body of knowledge and methodologies (calculi), for implementing real-world systems by trustworthy computer systems. Trustworthiness requires that all computer system components are theory based and have been verified relative the theory.

The distinction between method and methodology is made to indicate that a method is a collection of rules for achieving some goal, whereas a methodology is a systematized collection of formal rules for achieving some goal supported by sound theory.

Hence, to summarize, the paper is concerned with the controlled and systematic evolution from doctrine based system development to theory based system development, and the evolution of users from a doctrinal view of systems to a theory based view of systems. It tries to identify some concepts and computer based tools from both types of system which promote such evolution.


Information System Operational Semantic Functional Programming Language Algebraic Specification Conventional Mathematician 
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.


  1. 1.
    Aho A.V., Ullman J.D. Foundations of Computer Science. W.H. Freeman and Company, 1992.Google Scholar
  2. 2.
    Van Leeuwen J. (Ed.) Handbook of Theoretical Computer Science. Volume A: Algorithms and Complexity. Volume B: Formal Models and Semantics. Elsevier, 1990.Google Scholar
  3. 3.
    Swatman P.A., Swatman P.M.C. Formal Specification: An Analytic tool for (Management) Information Systems. Journal of Information Systems, Vol. 2, No.2, April 1992, 121–160.Google Scholar
  4. 4.
    Garland S.J., Guttag J.V., Horning J.J. An Overview of LARCH. In this volume.Google Scholar
  5. 5.
    Ophel John An Introduction to the High-Level Language Standard ML. In this volume.Google Scholar
  6. 6.
    Winkler Tim Programming in OBJ and Maude. In this volume.Google Scholar
  7. 7.
    Howe D.J. Reasoning About Functional Programs in Nuprl. In this volume.Google Scholar
  8. 8.
    Kromodimoeljo S., Pase Bill, Saaltink M., Craigen D., Meisels I. The EVES System. In this volume.Google Scholar
  9. 9.
    Malhotra J., Shapiro R.M. Generating an Algorithm for Executing Graphical Models. In this volume.Google Scholar
  10. 10.
    Shapiro R.M., Pinci V.O., Mameli R. Modeling a NORAD Command Post Using SADT and Colored Petri Nets. In this volume.Google Scholar
  11. 11.
    van Hee K.M., Rambags P.M.P, Verkoulen P.A.C. Specification and Simulation in ExSpect. In this volume.Google Scholar
  12. 12.
    MacQueen D.B. Reflections on Standard ML. In this volume.Google Scholar
  13. 13.
    Cleaveland R. Analyzing Concurrent Systems Using the Concurrency Workbench. In this volume.Google Scholar
  14. 14.
    Zucker J. Propositional Temporal Logics and their Use in Model Checking. In this volume.Google Scholar
  15. 15.
    Zucker J. The Propositional μ-Calculus and its Use in Model Checking. In this volume.Google Scholar
  16. 16.
    Lauer P.E. Computer System Dossiers. In Distributed Computing Systems, Academic Press, 1983, 109–147.Google Scholar
  17. 17.
    Lauer P.E., Campbell R.H. RECIPE: Requirements for an Evolutionary Computerbased Information Processing Environment. In Software Process Workshop, Egham U.K., 1984Google Scholar
  18. 18.
    Whiteside Fred GRIPE: A User Complaint and Maintainer Response System. Report on a Software Engineering Project, Dept. of Computer Science and Systems, McMaster University, Hamilton, Ontario, Canada, 1985.Google Scholar
  19. 19.
    Hoare C.A.R. Communicating Sequential Processes. Prentice-Hall, 1985.Google Scholar
  20. 20.
    Janicki R., Lauer P.E. Specification and Analysis of Concurrent Systems: The COSY Approach. Springer-Verlag, 1992.Google Scholar
  21. 21.
    Milner R., Tofte M., and Harper R. The Definition of Standard ML. The MIT Press, Cambridge, 1990.Google Scholar
  22. 22.
    Appel A. and MacQueen D. A standard ML compiler. In Functional Programming Languages and Computer Architecture, pages 301–324. Springer-Verlag Lecture Notes In Computer Science 274, 1987.Google Scholar
  23. 23.
    Gordon M.J.C. HOL: A Proof Generating System for Higher-Order Logic. In VLSI Specification, Verification and Synthesis, edited by G. Birtwistle and P.A. Subramanyam, Kluwer, 1988, 73–128.Google Scholar
  24. 24.
    Sannella D., Tarlecki A. Extended ML: an institution-independent framework for formal program development. Technical report, Report ECS-LFCS-86-16, Laboratory for Foundations of Computer Science, Computer Science Department, Edinburgh University, 1986.Google Scholar
  25. 25.
    Sannella D. Formal program development in Extended ML for the working programmer. Technical report, Report ECS-LFCS-89-102, Laboratory for Foundations of Computer Science, Computer Science Department, Edinburgh University, 1989.Google Scholar
  26. 26.
    Parnas D.L. Tabular Representation of Relations. Technical report, CRL Report No.260, Communications Research Laboratory, McMaster University, October 1992.Google Scholar
  27. 27.
    Parnas D.L. A technique for software module specification with examples. CACM 15, 5(1972), 330–336.Google Scholar
  28. 28.
    Parnas D.L. On the Criteria to be Used in Decomposing Systems into Modules. CACM 15, 12(1972), 1053–1058.Google Scholar
  29. 29.
    Reps T.W., Teitelbaum T. The Synthesizer Generator: A system for constructing language-based editors. Springer-Verlag, 1988.Google Scholar
  30. 30.
    Reps T.W., Teitelbaum T. The Synthesizer Generator: Reference Manual. Springer-Verlag, 1989.Google Scholar
  31. 31.
    Custeau R., Shelley C. Development of an Editor for Proving Theorems of First-order Logic. Senior Undergraduate Project, Department of Computer Science and Systems, McMaster University, 1990.Google Scholar
  32. 32.
    Pollack R. The Theory of LEGO. Manuscript, Laboratory for Foundations of Computer Science, Computer Science Department, Edinburgh University, 1988.Google Scholar
  33. 33.
    Luo Z., Pollack R., Taylor P. How to use LEGO. Preliminary User's Manual, Laboratory for Foundations of Computer Science, Computer Science Department, Edinburgh University, 1989.Google Scholar
  34. 34.
    Reppy J.H. Concurrent ML: Design, Application and Semantics. In this volume.Google Scholar
  35. 35.
    Reppy J.H. CML: A higher-order concurrent language. In SIGPLAN'91 Conference on Programming Language Design and Implementation, pages 293–305. SIGPLAN Notices 26(6), 1991.Google Scholar
  36. 36.
    Sanella D. A Survey of Formal Software Development Methods. Technical report, Report ECS-LFCS-88-56, Laboratory for Foundations of Computer Science, Computer Science Department, Edinburgh University, 1988.Google Scholar
  37. 37.
    Broy M., Geser A., Hussmann H. Towards Programming Environments Based on Algebraic Concepts. MIP-8826, Faculty of Mathematics and Informatik, University of Passau, 1988.Google Scholar
  38. 38.
    Dauchy P., Marre B. Test Data Selection from the Algebraic Specification of a Module of an Automatic Subway. Rapp. de Recherche no. 638, L.R.I. Universite de Paris Sud, 1991.Google Scholar
  39. 39.
    Bernot G., Gaudel M.C., Marre B. Software Testing Based on Formal Specifications: A Theory and a Tool. Rapp. de Recherche no. 581, L.R.I. Universite de Paris Sud, 1990.Google Scholar
  40. 40.
    Reisig W. Petri Nets: An Introduction. Springer-Verlag, 1985.Google Scholar
  41. 41.
    Ehrig H., Mahr B. Fundamentals of Algebraic Specification 2: Module Specifications and Constraints. Springer-Verlag, 1990.Google Scholar
  42. 42.
    Messeguer J. A Logical Theory of Concurrent Objects. SRI-CS-90-07, SRI International, Computer Science Laboratory, 1990.Google Scholar
  43. 43.
    Messeguer J. Conditional Rewriting Logic as a Unified Model of Concurrency. SRI-CS-91-05, SRI International, Computer Science Laboratory, 1991.Google Scholar
  44. 44.
    Paulson L.C. ML for the Working Programmer. Cambridge University Press, Cambridge, 1992.Google Scholar
  45. 45.
    Reade C. Elements of Functional Programming. Addison-Wesley, Reading, MA, 1989.Google Scholar
  46. 46.
    Hughes J. Why functional programming matters. The Computer Journal, 32(2):98–107, 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Peter E. Lauer
    • 1
  1. 1.Department of Computer Science and SystemsMcMaster UniversityHamiltonCanada

Personalised recommendations