×

Study of modular specifications. Constructions of finite colimits diagrams, isomorphisms. I. (Étude des spécifications modulaires. Constructions de colimites finies, diagrammes, isomorphismes. I.) (French) Zbl 0958.18001

A program specification is a description of program functionalities independently of realization. If one aims at program validation, automatic synthesis, systematic test production, one needs a formal specification.
Algebraic specifications are based on logic systems describing properties that any realization (model) must satisfy. An algebraic specification consists of a signature, containing the symbols used to construct terms, and of axioms defining properties of the terms. The underlying logic describes the set of theorems deducible from axioms. The semantics of algebraic specifications associates with each specification a class of models, namely a class of many-sorted algebras satisfying axioms. The formalism of algebraic specifications relies largely on category theory. Morphisms of specifications play an essential rôle, insofar as they express relations between specifications.
Now, the development of large specifications requires modularity, either top-down or bottom-up modularity. In the former case, the specification problem is decomposed into subproblems. In the latter case, complex specifications are constructed by suitable composition of basic modules. This is the approach the present work is interested in. Composition of specifications is expressed in a categorical framework by colimit constructions.
From a syntactic point of view, a language to represent modular specifications is defined, which is built from a category of base specifications and base specification morphisms. This language is formally characterized by a finitely cocomplete category of terms.
From a semantic point of view, a diagram is associated with each term. This interpretation permits to abstract some choices made while constructing a modular specification. Thus a “concrete” category of diagrams is defined. By considering the quotient by a suitable congruence relation, one gets a completion of the base category with finite colimits. Thus an equivalence between the category of terms and the category of diagrams is proved which shows the soundness of the interpretation.
Finally an algorithm is given to decide whether two diagrams are isomorphic, when the category is finite and cycle-free. This permits to detect “construction isomorphisms”, namely isomorphisms which do not depend on the base specification, but only on their combination.
The work is divided in three parts. The present article introduces algebraic specifications and gives the theoretical bases by defining the category of diagrams and concept of colimits.

MSC:

18C50 Categorical semantics of formal languages
68Q65 Abstract data types; algebraic specification
18A30 Limits and colimits (products, sums, directed limits, pushouts, fiber products, equalizers, kernels, ends and coends, etc.)
18A10 Graphs, diagram schemes, precategories
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

Simula 67
PDFBibTeX XMLCite
Full Text: EuDML

References:

[1] A. Asperti and G. Longo. Categories, Types and Structures, An Introduction to Category Theory for the Working Computer Scientist. Foundations of Computing Science, MIT Press, 1991. Zbl0783.18001 MR1159196 · Zbl 0783.18001
[2] M. A. Arbib and E. G. Manes. Arrows, Structures and Functors: The Categorical Imperative. Academic Press, 1975. Zbl0374.18001 MR364383 · Zbl 0374.18001
[3] D. Bert et al. Reference manual of the specification language LPG. Technical Report 59, LIFIA, Mars 1990. Anonymous ftp at imag.fr, in /pub/SC0P/LPG/NewSun4/man-lpg.dvi.
[4] G. Bernot, M. Bidoit, and C. Choppy. Abstract data types with exception handling: An initial approach based on a distinction between exception and errors. Theoretical Computer Science, 46(1) : 13-45, 1986. Zbl0603.68015 MR868261 · Zbl 0603.68015 · doi:10.1016/0304-3975(86)90019-8
[5] G. Birtwistle, O.-J. Dahl, B. Myrhaug, and K. Nygaard. Simula Begin. Auerbach Pub., New York, 1973.
[6] D. Bert and R. Echahed. Design and implementation of a generic, logic and functional programming language. In Proceedings of ESOP’86, number 213 in LNCS, pages 119-132. Springer-Verlag, 1986. Zbl0587.68003 · Zbl 0587.68003
[7] D. Bert. Refinements of generic specifications with algebraic tools. In Proceedings of IFIP’83, Paris, pages 815-820, 1983.
[8] D. Bert. Spécification de logiciels réutilisables. Technical Report RR-828-I-IMAG-116, LIFIA, Octobre 1990.
[9] R. M. Burstall and J. A. Goguen. Putting theories together to make specifications. In Proceedings of the 5th International Joint Conference on Artificial Intelligence, pages 1045-1058, 1977.
[10] R. M. Burstall and J. A. Goguen. The semantics of CLEAR, a specification language. In Proceedings of Advanced Course on Abstract Software Specification, number 86 in LNCS, pages 292-332. Springer-Verlag, 1980. Zbl0456.68024 · Zbl 0456.68024
[11] J. A. Bergstra, J. Heering, and R. Klint. Module algebra. J. ACM, 37(2) : 335-372, Apr. 1990. Zbl0696.68040 MR1072262 · Zbl 0696.68040 · doi:10.1145/77600.77621
[12] M. Bidoit. PLUSS, un langage pour le développement de spécifications algébriques modulaires, Mai 1989. Thèse d’Etat, Université de Paris-Sud.
[13] G. Bernot and P. Le Gall. Exception handling and term labelling. In Proceedings of TAPSOFT93, number 668 in LNCS, pages 421-436. Springer-Verlag, 1993. MR1252209
[14] D. Bert and C. Oriat. A model inference system for generic specification with application to code sharing. In Proceedings of TAPSOFT’95, number 915 in LNCS, pages 741-755. Springer-Verlag, 1995.
[15] R. M. Burstall and D. Rydeheard. Computing with categories. Technical Report ECS-LFCS-86-9, University of Edinburgh, September 1986. · Zbl 0616.68011
[16] R. M. Burstall. Electronic category theory. In Proceedings of the 9th Symposium on Mathematical Foundations of Computer Science, 1980. Zbl0462.68003 MR599553 · Zbl 0462.68003
[17] S. L. Bloom and E. G. Wagner. Many-sorted theories and their algebras with some applications to data types. In M. Nivat and J. C. Reynolds, editors, Algebraic Methods in Semantics, chapter 4, pages 133-168. Cambridge University Press, 1985. Zbl0575.18004 MR835451 · Zbl 0575.18004
[18] M. Barr and C. Wells. Category Theory for Computing Science. Prentice-Hall International, 1990. Zbl0714.18001 MR1094561 · Zbl 0714.18001
[19] M. Barr and C. Wells. The categorical theory generated by a limit sketch, Nov. 1994.
[20] J. Cartmell. Generalized algebraic theories and contextual categories. Annals of Pure and Applied Logic, 32:209-243, 1986. Zbl0634.18003 MR865990 · Zbl 0634.18003 · doi:10.1016/0168-0072(86)90053-9
[21] P. M. Cohn. Universal Algebra. Harper and Row, 1965. Revised version 1980. Zbl0141.01002 MR175948 · Zbl 0141.01002
[22] F. Cury. Catégories lax-localement-cartésiennes et catégories localement cartésiennes : un exemple de suffisante complétude connexe de sémantiques initiales. In diagrammes, volume 25, pages 1-155, Université Paris 7, Juillet 1991. Zbl0815.18004 MR1142466 · Zbl 0815.18004
[23] O.-J. Dahl and K. Nygaard. Simula - an Algol-based simulation language. Communications of the ACM, 9:671-678, Sept. 1966. Zbl0139.32903 · Zbl 0139.32903 · doi:10.1145/365813.365819
[24] D. Duval and J.-C. Reynaud. Sketches and computation (part 1): Basic definitions and static evaluation. Mathematical Structures in Computer Science, 4:185-238, 1994. Zbl0810.68096 MR1281759 · Zbl 0810.68096 · doi:10.1017/S0960129500000438
[25] D. Duval and J.-C. Reynaud. Sketches and computation (part 2): Dynamic evaluation and applications. Mathematical Structures in Computer Science, 4:239-271, 1994. Zbl0822.68063 MR1281760 · Zbl 0822.68063 · doi:10.1017/S096012950000044X
[26] C. Ehresmann. Esquisses et types de structures algébriques. Bulletin de l’institut Polytechnique, Iasi 14, 1968. Zbl0196.03102 MR238918 · Zbl 0196.03102
[27] H. Ehrig, R. M. Jimenez, and F. Orejas. Compositionality results for different types of parameterization and parameter passing in specification languages. In Proceedings of the 4th International Joint Conference CAAP/FASE, number 668 in LNCS, pages 31-45. Springer-Verlag, 1993.
[28] H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 1. Equations and Initial Semantics, volume 6 of EATCS Monographs on Theorectical Computer Sceince. Springer-Verlag, 1985. Zbl0557.68013 MR788495 · Zbl 0557.68013
[29] H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 2. Module Specifications and Constraints, volume 21 of EATCS Monographs on Theorectical Computer Science. Springer-Verlag, 1990. Zbl0759.68013 MR1036519 · Zbl 0759.68013
[30] K. Futatsugi, J. A. Goguen, J.-P. Jouannaud, and J. Meseguer. Principles of OBJ2. In Proceedings of Principles of Programming Languages, pages 52-66, 1985.
[31] M.-C. Gaudel. A first introduction to PLUSS. Technical report, Université d’Orsay, France, 1984.
[32] J. A. Goguen and R. M. Burstall. Introducing institutions. In Proceedings of the Workshop on Logic of Programming, number 164 in LNCS, pages 221-256. Springer-Verlag, 1984. Zbl0543.68021 MR778942 · Zbl 0543.68021
[33] J. A. Goguen and R. M. Burstall. Institutions: Abstract model theory for specification and programming. Research Report ECS-LFCS-90-106, University of Edinburgh, January 1990.
[34] J. A. Goguen, C. Kirchner, H. Kirchner, A. Mégrelis, J. Meseguer, and T. Winkler. An introduction to OBJ3. In Proceedings of the 1st International Workshop on Conditional Term Rewriting Systems, number 308 in LNCS, pages 258-263. Springer-Verlag, 1987. Zbl0666.68010 MR900615 · Zbl 0666.68010
[35] J. A. Goguen. Categorical foundations for general systems theory. In Advances in Cybernetics and System Research, pages 121-130. Transcripta Books, 1973.
[36] J. A. Goguen. Sheaf semantics for concurrent interacting objects. Mathematical Structures in Computer Science, 2:159-191, 1992. Zbl0763.18005 MR1171509 · Zbl 0763.18005 · doi:10.1017/S0960129500001420
[37] R. Goldblatt. Topoi: The Categorial Analysis of Logic, volume 98 of Studies in Logic and the Foundations of Mathematics. North Holland, 1979. Zbl0434.03050 MR551362 · Zbl 0434.03050
[38] J. A. Goguen, J. W. Thatcher, and E. G. Wagner. An initial algebra approach to the specification, correctness, and implementation of abstract data types. In R. T. Yeh, editor, Current Trends in Programming Methodology, volume 4: Data Structuring, pages 80-149. Prentice-Hall, 1978.
[39] J. A. Goguen, J. W. Thatcher, E. G. Wagner, and J. B. Wright. Abstract data types as initial algebras and the correctness of data representation. In Computer Graphics, Pattern Recognition and Data Structure, pages 89-93, 1975.
[40] J. A. Goguen, J. W. Thatcher, E. G. Wagner, and J. B. Wright. Initial algebra semantics and continuous algebra. J. ACM, 24:68-95, 1977. Zbl0359.68018 MR520711 · Zbl 0359.68018 · doi:10.1145/321992.321997
[41] J. V. Guttag. The specification and application to programming of abstract data types. PhD thesis, University of Toronto, 1975.
[42] J. V. Guttag. Abstract data types and the development of data structures. Communication of the ACM, 6:396-404, 1977. Zbl0356.68022 · Zbl 0356.68022 · doi:10.1145/359605.359618
[43] J.-M. Hufflen. Proposal for GLIDER version 1.0: Principles and main features. ICARUS Technical Report, INRIA-LORRAINE & CRIN, 1992.
[44] W. Lawvere. Functorial semantics of algebraic theories. Proc. Nat. Acad. Sci.. 50:869-873, 1963. Zbl0119.25901 MR158921 · Zbl 0119.25901 · doi:10.1073/pnas.50.5.869
[45] D. Lorge Parnas, P. C. Clements, and D. M. Weiss. The modular structure of complex systems. IEEE Transactions on Software Engineering, SE-11(3):259-266, March 1985.
[46] J. Lambek and P. J. Scott. Introduction to higher order categorical logic. Cambridge studies in advanced mathematics, 1986. Zbl0596.03002 MR856915 · Zbl 0596.03002
[47] B. Liskov and S. Zilles. Programming with abstract data types. ACM SIGPLAN Notices, 9(4):50-59, 1974.
[48] A. Martins. La généralisation: un outil pour la réutilisation. PhD thesis, INPG, Grenoble, Mars 1995.
[49] S. Mac Lane and G. Birkhoff. Algèbre. 1. Structures fondamentales. Gauthier-Villars, 1970. Zbl0201.01801 MR266716 · Zbl 0201.01801
[50] S. Mac Lane. Categories for the Working Mathematician. Springer-Verlag, 1971. Zbl0232.18001 MR1712872 · Zbl 0232.18001
[51] J. Meseguer and J. A. Goguen. Initiality, induction, and computability. In M. Nivat and J. C. Reynolds, editors, Algebraic Methods in Semantics, chapter 14, pages 459-541. Cambridge University Press, 1985. Zbl0571.68004 MR835461 · Zbl 0571.68004
[52] C. Oriat. Representing modular specifications as diagrams. In Compte Rendu des Journées du GDR Programmation, Lille, pages 53-68, Septembre 1994.
[53] C. Oriat. Detecting isomorphisms of modular specifications with diagrams. In Proceedings of AMAST’95, number 936 in LNCS, pages 184-198. Springer-Verlag, 1995.
[54] A. Poigné. Basic category theory. In Handbook of Logic in Computer Science, Volume 1. Background: Mathematical Structures, pages 413-640. Oxford Science Publication, 1992. MR1426366
[55] G. Renardel de Lavalette. Logical semantics of modularisation. In Proceedings of CSL ’91, number 626 in LNCS, pages 306-315. Springer-Verlag, 1991. Zbl0819.68079 MR1232896 · Zbl 0819.68079
[56] J.-C. Reynaud. Sémantique de LPG. Research Report 651 I IMAG, LIFIA, Mars 1987.
[57] J.-C. Reynaud. Putting algebraic components together: A dependent type approach. Research Report 810 I IMAG, LIFIA, Avril 1990. Extended version. MR1066214
[58] J.-C. Reynaud. Putting algebraic components together: A dependent type approach. In Proceedings of DISCO’90, number 429 in LNCS. Springer-Verlag, 1990. MR1066214
[59] J.-C. Reynaud. Isomorphism of typed algebraic specifications. Internal Report, LGI-IMAG, Avril 1993.
[60] R. A. G. Seely. Locally cartesian closed categories and type theory. Math. Proc. Camb. Phil. Soc, 95(33):33-48, 1984. Zbl0539.03048 MR727078 · Zbl 0539.03048 · doi:10.1017/S0305004100061284
[61] M. B. Smyth and G. D. Plotkin. The category-theoretic solution of recursive domain equations. In Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pages 13-17, 1977. MR488968
[62] D. Sannella, S. Sokolowski, and A. Tarlecki. Toward formal development of programs from algebraic specifications: Parameterisation revisited. Acta Informatica, 29:689-736, 1992. Zbl0790.68077 MR1202065 · Zbl 0790.68077 · doi:10.1007/BF01191893
[63] D. Sannella and A. Tarlecki. Specifications in an arbitrary institution. Information and Computation, 76:165-210, 1988. Zbl0654.68017 MR935895 · Zbl 0654.68017 · doi:10.1016/0890-5401(88)90008-9
[64] D. Sannella and M. Wirsing. A kernal language for algebraic specification and implementation. In Proceedings of the 11th Colloquium on Foundations of Computation Theory, number 158 in LNCS, pages 413-427. Springer-Verlag, 1983. Zbl0517.68043 MR734738 · Zbl 0517.68043
[65] T. Streicher and M. Wirsing. Dependent types considered necessary for specification languages. In Proceedings of the 7th Workshop on Specification of Abstract Data Types, number 534 in LNCS, pages 323-339, 1991.
[66] A. Tarlecki, R. M. Burstall, and J. A. Goguen. Some fundamental algebraic tools for the semantics of computation: Part 3. Indexed categories. Theoretical Computer Science, 91:239-264, 1991. Zbl0755.18004 MR1142330 · Zbl 0755.18004 · doi:10.1016/0304-3975(91)90085-G
[67] J. W. Thatcher, E. G. Wagner, and J. B. Wright. Data type specification: Parameterization and the power of specification techniques. ACM Trans. Prog. Lang. Syst., 4:711-773, 1982. Zbl0495.68020 MR521047 · Zbl 0495.68020 · doi:10.1145/69622.357192
[68] M. Wand. Fixed-point constructions in order-enriched categories. Theoretical Computer Science, 8:13-30, 1979. Zbl0401.18005 MR523657 · Zbl 0401.18005 · doi:10.1016/0304-3975(79)90053-7
[69] E. G. Wagner, S. L. Bloom, and J. W. Thatcher. Why algebraic theories? In M. Nivat and J. C. Reynolds, editors, Algebraic Methods in Semantics, chapter 17, pages 607-634. Cambridge University Press, 1985. Zbl0637.68019 MR835464 · Zbl 0637.68019
[70] M. Wirsing. Structured algebraic specifications: A kernel language. Theoretical Computer Science, 42:123-249, 1986. Zbl0599.68021 MR858687 · Zbl 0599.68021 · doi:10.1016/0304-3975(86)90051-4
[71] M. Wirsing. Algebraic specification. In J. van Leeuwen, editor, Hand-book of Theoretical Computer Science, chapter 13, pages 677-788. Elsevier Science Publishers B.V., 1990. Zbl0900.68309 MR1127198 · Zbl 0900.68309
[72] M. Wirsing. Algebraic specification languages: An overview. In Recent Trends in Data Type Specification. 10th Workshop on Specification of Abstract Data Types, number 906 in LNCS, 1994.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.