Sannella, Donald; Tarlecki, Andrzej Specifications in an arbitrary institution. (English) Zbl 0654.68017 Inf. Comput. 76, No. 2-3, 165-210 (1988). Based on the work on algebraic specification, there are quite a few specification languages supporting structured ways of building large and complex specifications by putting together small ones. Only one of these languages, CLEAR, is based on arbitrary institutions, providing maximum generality and flexibility. The other languages, however, include features not included in CLEAR which make them more useful as tools for writing specifications in the particular institution they treat. The goal of the paper is to present a general institution-based specification approach which incorporates the good ideas of all these languages. One of the main contributions of this paper is to provide an institution- based specification-building operation of behavioural abstraction. After a concise introduction to institutions in section 2, section 3 shows how free variables can be introduced into the sentences of an institution and how quantifiers can be added which bind them. This way, also unreachable elements of models can be named, and this is necessary for dealing appropriately with behavioural abstraction. In section 4, a set of primitive operations for building specifications in an arbitrary institution is defined. These operations are loosely based on those of ASL and consist of the following: - Form a basic specification, given a signature \(\Sigma\) and set \(\Phi\) of \(\Sigma\)-sentences. - Form the union of a family of \(\Sigma\)-specifications. - Translate a \(\Sigma\)-specification to another signature \(\Sigma\) ’ along a signature morphism \(\sigma\) : \(\Sigma\) \(\to \Sigma '.\) - Derive a \(\Sigma\) ’-specification from a specification over a richer signature \(\Sigma\) using a signature morphism \(\sigma\) : \(\Sigma\) ’\(\to \Sigma.\) - Given a \(\Sigma\)-specification, restrict models to only those which are minimal extension of their \(\sigma\)-reducts for a given \(\sigma\) : \(\Sigma\) ’\(\to \Sigma.\) - Close a collection of models under isomorphism. - Abstract away from certain details of a specification, admitting only models which are equivalent to a model of the specification w.r.t. some given set of properties. The latter is the above mentioned behavioural abstraction. These operations are meant to be low-level, not for use directly in a specification language but useful for defining convenient-to-use specification-building operations of high-level languages. Operations having to do with free generation, e.g., initially, are missing because they do not generalize to arbitrary institutions. In section 5, the general definitions are instantiated with two different institutions: first-order logic with equality, and partial first-order logic. The resulting operations are compared with those found in existing specification languages. In section 6, the authors consider the problem of theorem proving in the context of specifications built using the operations defined in section 4. An approach is presented which enables the structure of proofs to reflect and exploit the structure of specifications. Inference rules are provided for each of the specification-building operations which are independent of the particular institution in use. It is shown that they are sound, and their completeness is analyzed. Section 7 presents a mechanism for defining and applying parameterized specifications. Section 8 concludes with remarks concerning the development of programs from specifications by stepwise refinement in this framework and the generality of the approach. The paper is very well written, a pleasure to read, and it contains useful information. Reading is strongly recommended to everybody interested in the foundations of formal, especially algebraic, approaches to software specification and development. Reviewer: H.-D.Ehrich Cited in 2 ReviewsCited in 75 Documents MSC: 68N01 General topics in the theory of software 68P05 Data structures 68Q65 Abstract data types; algebraic specification 03B10 Classical first-order logic 68Q60 Specification and verification (program logics, model checking, etc.) 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) Keywords:algebraic specification; specification languages; institutions; free variables; first-order logic; theorem proving Citations:Zbl 0552.68015 PDFBibTeX XMLCite \textit{D. Sannella} and \textit{A. Tarlecki}, Inf. Comput. 76, No. 2--3, 165--210 (1988; Zbl 0654.68017) Full Text: DOI References: [1] Abrial, J. R.; Schuman, S. A.; Meyer, B., Specification language Z (1979), Massachusetts Computer Associates Inc: Massachusetts Computer Associates Inc Boston · Zbl 0413.68024 [2] Adamek, J.; Nelson, E.; Reiterman, J., A Birkhoff variety theorem for continuous algebras, Algebra Universalis, 20, 328-350 (1985) · Zbl 0594.08005 [3] Arbib, M. A.; Manes, E. G., (Arrows, Structures and Functors: The Categorical Imperative (1975), Academic Press: Academic Press New York) · Zbl 0374.18001 [4] Barwise, K. J., Axioms for abstract model theory, Ann. of Math. Logic, 7, 221-265 (1974) · Zbl 0324.02034 [5] Bauer, F. L., (Report on a Wide Spectrum Language for Program Specification and Development (1981), Technische Univ: Technische Univ München), Report TUM-18104 [6] Benecke, K.; Reichel, H., Equational partiality, Algebra Universalis, 16, 219-232 (1983) · Zbl 0524.08005 [7] Bergstra, J. A.; Broy, M.; Tucker, J. V.; Wirsing, M., On the power of algebraic specifications, (Proc. 10th Intl. Symp. on Mathematical Foundations of Computer Science. Proc. 10th Intl. Symp. on Mathematical Foundations of Computer Science, Strbske Pleso, Czechoslovakia. Proc. 10th Intl. Symp. on Mathematical Foundations of Computer Science. Proc. 10th Intl. Symp. on Mathematical Foundations of Computer Science, Strbske Pleso, Czechoslovakia, Lecture Notes in Computer Science, Vol. 118 (1981), Springer-Verlag: Springer-Verlag Berlin/New York), 193-204 · Zbl 0462.68001 [8] Bergstra, J. A.; Meyer, J. J., I/O computable data structures, SIGPLAN Notices, 16, 4, 27-32 (1981) [9] Bloom, S. L.; Wagner, E. G., Many-sorted theories and their algebras with some applications to data types, (Nivat, M.; Reynolds, J. C., Algebraic Methods in Semantics (1985), Cambridge Univ. Press) · Zbl 0575.18004 [10] Broy, M.; Wirsing, M., Partial abstract types, Acta Inform., 18, 47-64 (1982) · Zbl 0494.68020 [11] Burmeister, P., Partial algebras—Survey of a unifying approach towards a two-valued model theory for partial algebras, Algebra Universalis, 15, 306-358 (1982) · Zbl 0511.03014 [12] Burstall, R. M.; Goguen, J. A., The semantics of Clear, a specification language, (Proc. of Advanced Course on Abstract Software Specifications. Proc. of Advanced Course on Abstract Software Specifications, Copenhagen. Proc. of Advanced Course on Abstract Software Specifications. Proc. of Advanced Course on Abstract Software Specifications, Copenhagen, Lecture Notes in Computer Science, Vol. 86 (1980), Springer-Verlag: Springer-Verlag Berlin/New York), 292-332 · Zbl 0456.68024 [13] Burstall, R. M.; Goguen, J. A., An informal introduction to specifications using Clear, (Boyer, R. S.; Moore, J. S., The Correctness Problem in Computer Science (1981), Academic Press: Academic Press New York), 185-213 [14] Clarke, E. M., Programming language constructs for which it is impossible to obtain good Hoare axiom systems, J. Assoc. Comput. Mach., 26, 1, 129-147 (1979) · Zbl 0388.68008 [15] Ehrich, H.-D., J. Assoc. Comput. Mach., 29, 1, 206-227 (1982) [16] Ehrig, H.; Fey, W.; Hansen, H., (ACT ONE: An Algebraic Specification Language with Two Levels of Semantics (1983), Institut für Software und Theoretische Informatik, Technische Univ: Institut für Software und Theoretische Informatik, Technische Univ Berlin), Report No. 83-03 · Zbl 0549.68010 [17] Ehrig, H.; Kreowski, H.-J.; Mahr, B.; Padawitz, P., Algebraic implementation of abstract data types, Theoret. Comput. Sci., 20, 209-263 (1982) · Zbl 0483.68018 [18] Ehrig, H.; Kreowski, H.-J.; Thatcher, J. W.; Wagner, E. G.; Wright, J. B., Parameterized data types in algebraic specification languages (short version), (Proc. 7th Intl. Colloq. on Automata, Languages and Programming. Proc. 7th Intl. Colloq. on Automata, Languages and Programming, Noordwijkerhout, Netherlands. Proc. 7th Intl. Colloq. on Automata, Languages and Programming. Proc. 7th Intl. Colloq. on Automata, Languages and Programming, Noordwijkerhout, Netherlands, Lecture Notes in Computer Science, Vol. 85 (1980), Springer-Verlag: Springer-Verlag Berlin/New York) · Zbl 0456.68101 [19] Ehrig, H.; Thatcher, J. W.; Lucas, P.; Zilles, S. N., Denotational and Initial Algebra Semantics of the Algebraic Specification Language Look (1982), Draft report, IBM research [20] Ehrig, H.; Wagner, E. G.; Thatcher, J. W., Algebraic specifications with generating constraints, (Proc. 10th ICALP. Proc. 10th ICALP, Barcelona. Proc. 10th ICALP. Proc. 10th ICALP, Barcelona, Lecture Notes in Computer Science, Vol. 154 (1983), Springer-Verlag: Springer-Verlag Berlin/New York), 188-202 · Zbl 0518.68019 [21] Gaudel, M. C., An introduction to PLUSS (1984), Université de Paris-Sud: Université de Paris-Sud Orsay, Draft report [22] Giarratana, V.; Gimona, F.; Montanari, U., Observability concepts in abstract data type specification, (Proc. 5th Intl. Symp. on Mathematical Foundations of Computer Science. Proc. 5th Intl. Symp. on Mathematical Foundations of Computer Science, Gdansk. Proc. 5th Intl. Symp. on Mathematical Foundations of Computer Science. Proc. 5th Intl. Symp. on Mathematical Foundations of Computer Science, Gdansk, Lecture Notes in Computer Science, Vol. 45 (1976), Springer-Verlag: Springer-Verlag Berlin/New York) · Zbl 0338.68023 [23] Gogolla, M.; Drosten, K.; Lipeck, U.; Ehrich, H.-D., Theoret. Comput. Sci., 34, 289-313 (1984) [24] Goguen, J. A., Abstract errors for abstract data types, (Proc. IFIP Working Conf. on the Formal Description of Programming Concepts. Proc. IFIP Working Conf. on the Formal Description of Programming Concepts, New Brunswick, NJ (1977)) · Zbl 0373.68024 [25] Goguen, J. A., (Order Sorted Algebras: Expectations and Error Sorts, Coercions and Overloaded Operators (1978), Department of Computer Science, UCLA), Semantics and Theory of Computation Report No. 14 · Zbl 0306.68028 [26] Goguen, J. A.; Burstall, R. M., Introducing institutions, (Clarke, E.; Kozen, D., Proc. Logics of Programming Workshop. Proc. Logics of Programming Workshop, Lecture Notes in Computer Science, Vol. 164 (1984), Springer-Verlag: Springer-Verlag Berlin/New York), 221-256, Carnegie-Mellon University · Zbl 0543.68021 [27] Goguen, J. A.; Burstall, R. M., Some fundamental algebraic tools for the semantics of computation. Part 1. Comma categories, colimits, signatures and theories, Theoret. Comput. Sci., 31, 175-210 (1984) · Zbl 0566.68065 [28] Goguen, J. A.; Meseguer, J., Universal realization, persistent interconnection and implementation of abstract modules, (Proc. 9th ICALP. Proc. 9th ICALP, Aarhus, Denmark. Proc. 9th ICALP. Proc. 9th ICALP, Aarhus, Denmark, Lecture Notes in Computer Science, Vol. 140 (1982), Springer-Verlag: Springer-Verlag Berlin/New York), 265-281 · Zbl 0493.68014 [29] Goguen, J. A.; Meseguer, J., (An Initiality Primer (1983), SRI International), Draft report [30] (Yeh, R. T., Current Trends in Programming Methodology, Vol. 4 (1978), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ), 80-149, Data Structuring [31] Guttag, J. V.; Horning, J. J., (Preliminary Report on the Larch Shared Language (1983), Computer Science Laboratory, Xerox PARC), Report CSL-83-6 · Zbl 0581.68007 [32] Kamin, S., Final data types and their specification, TOPLAS, 5, 1, 97-121 (1983) · Zbl 0498.68008 [33] Liskov, B.; Atkinson, R.; Bloom, T.; Moss, E.; Schaffert, J. C.; Scheifler, R.; Snyder, A., CLU Reference Manual, (Lecture Notes in Computer Science, Vol. 144 (1981), Springer-Verlag: Springer-Verlag Berlin/New York) · Zbl 0463.68009 [34] Liskov, B. H.; Berzins, V., (An Appraisal of Program Specifications (1977), Laboratory for Computer Science, MIT), Computation structures group memo 141-1 [35] MacLane, S., (Categories for the Working Mathematician (1971), Springer-Verlag: Springer-Verlag Berlin/New York) [36] MacQueen, D. B.; Sannella, D. T., Completeness of proof systems for equational specifications, IEEE Trans. Software Engrg., SE-11, 454-461 (1985) · Zbl 0558.68017 [37] Mahr, B.; Makowsky, J. A., Characterizing specification languages which admit initial semantics, Theoret. Comput. Sci., 31, 49-60 (1984) · Zbl 0536.68011 [38] Makowsky, J. A., Why Horn formulas matter in computer science: Initial structures and generic examples, (Proc. 10th Colloq. on Trees in Algebra and Programming, Joint Conf. on Theory and Practice of Software Development (TAPSOFT). Proc. 10th Colloq. on Trees in Algebra and Programming, Joint Conf. on Theory and Practice of Software Development (TAPSOFT), Berlin. Proc. 10th Colloq. on Trees in Algebra and Programming, Joint Conf. on Theory and Practice of Software Development (TAPSOFT). Proc. 10th Colloq. on Trees in Algebra and Programming, Joint Conf. on Theory and Practice of Software Development (TAPSOFT), Berlin, Lecture Notes in Computer Science (1985), Springer-Verlag: Springer-Verlag Berlin/New York), 374-387 · Zbl 0619.68029 [39] Milner, R. G., A proposal for Standard ML, (Proc. 1984 ACM Symp. on LISP and Functional Programming. Proc. 1984 ACM Symp. on LISP and Functional Programming, Austin, Texas (1984)) [40] Moore, E. F., Gedanken-experiments on sequential machines, (Shannon, C. E.; McCarthy, J., Automata Studies (1956), Princeton Univ. Press: Princeton Univ. Press Princeton), 129-153 [41] Pepper, P., On the correctness of type transformations, (talk at 2nd Workshop on Theory and Applications of Abstract Data Types. talk at 2nd Workshop on Theory and Applications of Abstract Data Types, Passau (1983)) · Zbl 0408.68074 [42] Reichel, H., Behavioural equivalence—A unifying concept for initial and final specification methods, (Proc. 3rd Hungarian Computer Science Conference. Proc. 3rd Hungarian Computer Science Conference, Budapest (1981)), 27-39 · Zbl 0479.68017 [43] Reichel, H., (Initial Computability, Algebraic Specifications, and Partial Algebras (1987), Oxford Univ. Press) · Zbl 0634.68001 [44] Sadler, M., Mapping out specification, (Workshop on Formal Aspects of Specification. Workshop on Formal Aspects of Specification, Swindon (1984)), Position paper [45] Sannella, D. T.; Burstall, R. M., Structured theories in LCF, (Proc. 8th Colloq. on Trees in Algebra and Programming. Proc. 8th Colloq. on Trees in Algebra and Programming, L’Aquila, Italy. Proc. 8th Colloq. on Trees in Algebra and Programming. Proc. 8th Colloq. on Trees in Algebra and Programming, L’Aquila, Italy, Lecture Notes in Computer Science, Vol. 159 (1983), Springer-Verlag: Springer-Verlag Berlin/New York), 377-391 · Zbl 0527.68070 [46] Sannella, D. T.; Tarlecki, A., Building specifications in an arbitrary institution, (Proc. Intl. Symposium on Semantics of Data Types. Proc. Intl. Symposium on Semantics of Data Types, Sophia-Antipolis. Proc. Intl. Symposium on Semantics of Data Types. Proc. Intl. Symposium on Semantics of Data Types, Sophia-Antipolis, Lecture Notes in Computer Science (1984), Springer-Verlag: Springer-Verlag Berlin/New York), 337-356 · Zbl 0552.68015 [47] Sannella, D. T.; Tarlecki, A., Program specification and development in Standard ML, (Proc 12th ACM Symp. on Principles of Programming Languages. Proc 12th ACM Symp. on Principles of Programming Languages, New Orleans (1985)), 67-77 [48] Sannella, D. T.; Tarlecki, A., (Proc. 10th Colloq. on Trees in Algebra and Programming, Joint Conf. on Theory and Practice of Software Development (TAPSOFT). Proc. 10th Colloq. on Trees in Algebra and Programming, Joint Conf. on Theory and Practice of Software Development (TAPSOFT), Berlin. Proc. 10th Colloq. on Trees in Algebra and Programming, Joint Conf. on Theory and Practice of Software Development (TAPSOFT). Proc. 10th Colloq. on Trees in Algebra and Programming, Joint Conf. on Theory and Practice of Software Development (TAPSOFT), Berlin, Lecture Notes in Computer Science, Vol. 185 (1985), Springer-Verlag: Springer-Verlag Berlin/New York), 308-322 · Zbl 0619.68028 [49] Sannella, D. T.; Wirsing, M., (Proc. Intl. Conf. on Foundations of Computation Theory. Proc. Intl. Conf. on Foundations of Computation Theory, Borgholm, Sweden. Proc. Intl. Conf. on Foundations of Computation Theory. Proc. Intl. Conf. on Foundations of Computation Theory, Borgholm, Sweden, Lecture Notes in Computer Science, Vol. 158 (1983), Springer-Verlag: Springer-Verlag Berlin/New York), 413-427 [50] Schoett, O., (A Theory of Program Modules, Their Specification and Implementation (1982), Department of Computer Science, Univ. of Edinburgh), Report CSR-155-83 [51] Sufrin, B., Formal specification of a display-oriented text editor, Sci. Comput. Programming, 1, 157-202 (1982) · Zbl 0479.68030 [52] Tarlecki, A., Free constructions in algebraic institutions, (Report CSR-149-83 (1983)) [53] Tarlecki, A., On the existence of free models in abstract algebraic institutions, Theoret. Comput. Sci., 37, 269-304 (1985) · Zbl 0608.68014 [54] Tarlecki, A., Quasi-varieties in abstract algebraic institutions, J. Comput. Syst. Sci., 33, 333-360 (1986) · Zbl 0622.68033 [55] Tarlecki, A.; Wirsing, M., Continuous abstract data types—Basic machinery and results, (Proc. Intl. Conf. on Fundamentals of Computation Theory. Proc. Intl. Conf. on Fundamentals of Computation Theory, Cottbus, GDR. Proc. Intl. Conf. on Fundamentals of Computation Theory. Proc. Intl. Conf. on Fundamentals of Computation Theory, Cottbus, GDR, Lecture Notes in Computer Science, Vol. 199 (1985), Springer-Verlag: Springer-Verlag Berlin/New York), 431-441 · Zbl 0571.68014 [56] Wand, M., Final algebra semantics and data type extensions, J. Comput. System Sci., 19, 27-44 (1979) · Zbl 0418.68020 [57] Wirsing, M., Structured algebraic specifications, (Proc. AFCET Symp. on Mathematics for Computer Science. Proc. AFCET Symp. on Mathematics for Computer Science, Paris (1982)), 93-107 [58] Wirsing, M., Structured Algebraic Specifications: A Kernel Language, (Habilitation thesis (1983), Technische Univ: Technische Univ München) · Zbl 0599.68021 [59] Zilles, S. N.; Lucas, P.; Thatcher, J. W., A Look at Algebraic Specifications (1982), IBM research report RJ 3568 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.