On the use of theory based systems to traverse educational gaps in computer system related activities
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.
KeywordsInformation System Operational Semantic Functional Programming Language Algebraic Specification Conventional Mathematician
Unable to display preview. Download preview PDF.
- 1.Aho A.V., Ullman J.D. Foundations of Computer Science. W.H. Freeman and Company, 1992.Google Scholar
- 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.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.Garland S.J., Guttag J.V., Horning J.J. An Overview of LARCH. In this volume.Google Scholar
- 5.Ophel John An Introduction to the High-Level Language Standard ML. In this volume.Google Scholar
- 6.Winkler Tim Programming in OBJ and Maude. In this volume.Google Scholar
- 7.Howe D.J. Reasoning About Functional Programs in Nuprl. In this volume.Google Scholar
- 8.Kromodimoeljo S., Pase Bill, Saaltink M., Craigen D., Meisels I. The EVES System. In this volume.Google Scholar
- 9.Malhotra J., Shapiro R.M. Generating an Algorithm for Executing Graphical Models. In this volume.Google Scholar
- 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.van Hee K.M., Rambags P.M.P, Verkoulen P.A.C. Specification and Simulation in ExSpect. In this volume.Google Scholar
- 12.MacQueen D.B. Reflections on Standard ML. In this volume.Google Scholar
- 13.Cleaveland R. Analyzing Concurrent Systems Using the Concurrency Workbench. In this volume.Google Scholar
- 14.Zucker J. Propositional Temporal Logics and their Use in Model Checking. In this volume.Google Scholar
- 15.Zucker J. The Propositional μ-Calculus and its Use in Model Checking. In this volume.Google Scholar
- 16.Lauer P.E. Computer System Dossiers. In Distributed Computing Systems, Academic Press, 1983, 109–147.Google Scholar
- 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.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.Hoare C.A.R. Communicating Sequential Processes. Prentice-Hall, 1985.Google Scholar
- 20.Janicki R., Lauer P.E. Specification and Analysis of Concurrent Systems: The COSY Approach. Springer-Verlag, 1992.Google Scholar
- 21.Milner R., Tofte M., and Harper R. The Definition of Standard ML. The MIT Press, Cambridge, 1990.Google Scholar
- 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.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.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.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.Parnas D.L. Tabular Representation of Relations. Technical report, CRL Report No.260, Communications Research Laboratory, McMaster University, October 1992.Google Scholar
- 27.Parnas D.L. A technique for software module specification with examples. CACM 15, 5(1972), 330–336.Google Scholar
- 28.Parnas D.L. On the Criteria to be Used in Decomposing Systems into Modules. CACM 15, 12(1972), 1053–1058.Google Scholar
- 29.Reps T.W., Teitelbaum T. The Synthesizer Generator: A system for constructing language-based editors. Springer-Verlag, 1988.Google Scholar
- 30.Reps T.W., Teitelbaum T. The Synthesizer Generator: Reference Manual. Springer-Verlag, 1989.Google Scholar
- 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.Pollack R. The Theory of LEGO. Manuscript, Laboratory for Foundations of Computer Science, Computer Science Department, Edinburgh University, 1988.Google Scholar
- 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.Reppy J.H. Concurrent ML: Design, Application and Semantics. In this volume.Google Scholar
- 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.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.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.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.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.Reisig W. Petri Nets: An Introduction. Springer-Verlag, 1985.Google Scholar
- 41.Ehrig H., Mahr B. Fundamentals of Algebraic Specification 2: Module Specifications and Constraints. Springer-Verlag, 1990.Google Scholar
- 42.Messeguer J. A Logical Theory of Concurrent Objects. SRI-CS-90-07, SRI International, Computer Science Laboratory, 1990.Google Scholar
- 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.Paulson L.C. ML for the Working Programmer. Cambridge University Press, Cambridge, 1992.Google Scholar
- 45.Reade C. Elements of Functional Programming. Addison-Wesley, Reading, MA, 1989.Google Scholar
- 46.Hughes J. Why functional programming matters. The Computer Journal, 32(2):98–107, 1989.Google Scholar