Module algebra

ABSTRACT

An axiomatic algebraic calculus of modules is given that is based on the operators combination/union, export, renaming, and taking the visible signature. Four different models of module algebra are discussed and compared.

REFERENCES

• 1: BERGSTRA, J.m. lermmologte van AtgeOratsctte ~pec~tcattes. t~auwer, L)eventer, I ne Nemerlantas, 1987 (in Dutch).
• 2: J. A. Bergstra , Jan Heering , Paul Klint, Algebraic specification, ACM Press, New York, NY, 1989
• 3: BERGSTRA, J. A., KLEIJN, H. C. M., AND NOUWT, P. On the algebraic specification of infinite data types using monoidal auxiliary functions. Rep. 80-43. Institute of Applied Mathematics and Computer Science, Univ. Leiden, Leiden, The Netherlands, 1980.
• 4: BERGSTRA, J. A., AND MEYER, J.-J. CH. Small specifications for large finite data structures. Internat. J. Comput. Math. 9, 4 (1981), 305-320.
• 5: BERGSTRA, J. A., AND MEYER, J.-J. CH. The equational specification of finite minimal unoids using unary hidden functions only. Fund. Inf. V, 2 (1982), 143-170.
• 6: BERGSTRA, J. A., AND MEYER, J.-J. CH. On specifying sets of integers. Elektronische Informationsverarbeitung und Kybernetik 20, 10/11 (1984), 531-541.
• 7: Jan A. Bergstra , J. V. Tucker, A Characterisation of Computable Data Types by Means of a Finite Equational Specification Method, Proceedings of the 7th Colloquium on Automata, Languages and Programming, p.76-90, July 14-18, 1980
• 8: BERGSTRA, J. A., AND TUCKER, J.V. The completeness of the algebraic specification methods for computable data types. Inf. Control 54, 3 (1982), 186-200.
• 9: BERGSTRA, J. A., AND TUCKER, J.V. Initial and final algebra semantics for data type specifications: Two characterization theorems. SIAM J. Comput. 12, 2 (1983), 366-387.
• 10: J. A. Bergstra , J. V. Tucker, Algebraic specifications of computable and semicomputable data types, Theoretical Computer Science, v.50 n.2, p.137-181, 1987 [doi>10.1016/0304-3975(87)90123-X]
• 11: E. K. Blum , H. Ehrig , F. Parisi-Presicce, Algebraic specification of modules and their basic interconnections, Journal of Computer and System Sciences, v.34 n.2-3, p.293-339, April/June 1987 [doi>10.1016/0022-0000(87)90028-6]
• 12: George S. Boolos , Richard C. Jeffrey, Computability and logic: 3rd ed., Cambridge University Press, New York, NY, 1989
• 13: Rod M. Burstall , Joseph A. Goguen, The Semantics of CLEAR, A Specification Language, Proceedings of the Abstract Software Specifications, 1979 Copenhagen Winter School, p.292-332, January 22-February 02, 1979
• 14: CHANG, C. C., AND KEISLER, H.j. Model Theory. North-Holland, Amsterdam, The Netherlands, 1973.
• 15: CRAIG, W. Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symb. Logic 22 (1957), 269-285.
• 16: H.-D. Ehrich, On the Theory of Specification, Implementation, and Parametrization of Abstract Data Types, Journal of the ACM (JACM), v.29 n.1, p.206-227, Jan. 1982 [doi>10.1145/322290.322303]
• 17: H. Ehrig , Bernd Mahr, Fundamentals of algebraic specification 2: module specifications and constraints, Springer-Verlag New York, Inc., New York, NY, 1990
• 18: Kokichi Futatsugi , Joseph A. Goguen , Jean-Pierre Jouannaud , José Meseguer, Principles of OBJ2, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.52-66, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318610]
• 19: GANZINGER, H. Increasing modularity and language-independency in automatically generated compilers. Sci. Comput. Prog. 3 (1983), 223-278.
• 20: GAUDEL, M.-C. Toward structured algebraic specifications. In Esprit '85: Status Report of Continuing Work, vol. 1. North-Holland, Amsterdam, 1986, pp. 493-510.
• 21: Joseph A. Goguen , Rod M. Burstall, Introducing Institutions, Proceedings of the Carnegie Mellon Workshop on Logic of Programs, p.221-256, June 06-08, 1983
• 22: Joseph A. Goguen , José Meseguer, Universal Realization, Persistent Interconnection and Implementation of Abstract Modules, Proceedings of the 9th Colloquium on Automata, Languages and Programming, p.265-281, July 12-16, 1982
• 23: J Heering, Partial evaluation and &ohgr;-completeness of algebraic specifications, Theoretical Computer Science, v.43 n.2-3, p.149-167, July 1986
• 24: J J Horning, Combining algebraic and predicative specifications in Larch, Proceedings of the International Joint Conference on Theory and Practice of Software Development (TAPSOFT) on Formal Methods and Software, Vol.2: Colloquium on Software Engineering (CSE), p.12-26, June 1985, Berlin, Germany
• 25: T M V Janssen, Foundations and applications of Montague grammar: 8M part 1: philosophy, framework, computer science, Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands, 1986
• 26: KAPLAN, S. Un langage de sprcification de types abstraits algrbriques. Thrse de 36me cycle. Universit6 de Paris-Sud, Paris, France, 1983 {in French}.
• 27: KLAEREN, H.A. Algebraische Spezifikation. Springer-Verlag, Berlin, 1983 {in German}.
• 28: KLEENE, S. C. Finite axiomatizability of theories in the predicate calculus using additional predicate symbols. Memoirs of the American Mathematical Society 10 (1952), 27-68. (Second printing, with revisions, American Mathematical Society, Providence, R.I., 1967.)
• 29: T. Lehmann, The specification language of Obscure, Lecture notes in Computer Science on Recent trends in data type specification, p.131-153, August 1988, Gullane, Scotland
• 30: LIPECK, U. Ein algebraischer Kalkiil for einen strukturierten Entwurf von Datenabstraktionen. Dissertation, Forschungsbericht Nr. 148, Abteilung Informatik, Universit~t Dortmund, Dortmund, BRD, 1983 {in German}.
• 31: T. S. E. Maibaum , M. R. Sadler, Axiomatizing Specification Theory, Selected Papers from the 3rd Workshop on Theory and Applications of Abstract Data Types: Recent Trends in Data Type Specification, p.171-177, November 13-16, 1984
• 32: T S E Maibaum , P A S Veloso , M R Sadler, A theory of abstract data types for program development: bridging the gap?, Proceedings of the International Joint Conference on Theory and Practice of Software Development (TAPSOFT) on Formal Methods and Software, Vol.2: Colloquium on Software Engineering (CSE), p.214-230, June 1985, Berlin, Germany
• 33: Limits of the "algebraic" specification of abstract data types, ACM SIGPLAN Notices, v.12 n.10, p.37-42, October 1977 [doi>10.1145/954627.954630]
• 34: J Meseguer , J A Goguen, Initiality, induction, and computability, Algebraic methods in semantics, Cambridge University Press, New York, NY, 1986
• 35: Francesco Parisi-Presicce, Union and actualization of module specifications: some compatibility results, Journal of Computer and System Sciences, v.35 n.1, p.72-95, Aug. 1987 [doi>10.1016/0022-0000(87)90037-7]
• 36: D. L. Parnas, On the criteria to be used in decomposing systems into modules, Communications of the ACM, v.15 n.12, p.1053-1058, Dec. 1972 [doi>10.1145/361598.361623]
• 37: RENARDEL DE LAVALETTE. G.R. Modularisation, parameterisation, interpolation. Logic Group Preprint Series No. 32, Department of Philosophy, University of Utrecht, Utrecht, The Netherlands, 1988.
• 38: RENARDEL DE LAVALETTE, G.R. Preliminary remarks on theories and interpolation. Unpublished note, July 20, 1988.
• 39: RODENBURG, P. H., AND VAN GLABBEEK, R.J. An interpolation theorem in equational logic. Report CS-R8838, Department of Computer Science, Centre for Mathematics and Computer Science, Amsterdam, The Netherlands, 1988.
• 40: SHOENFIELD, J.R. Mathematical Logic. Addison-Wesley, Reading, Mass., 1967.
• 41: WmSING, M. Structured algebraic specifications: A kernel language. Thesis, Institut f/Jr Informatik, Technische Universit~it, Miinchen, BRD, 1983.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs
      F.3.2 Semantics of Programming Languages
          Subjects: Algebraic approaches to semantics

General Terms:
Languages, Theory