×

Toward formal development of programs from algebraic specifications: Implementations revisited. (English) Zbl 0621.68004

The program development process is viewed as a sequence of implementation steps leading from a specification to a program. Based on an elementary notion of refinement, two notions of implementation are studied: constructor implementations which involve a construction ”on top of” the implementing specification, and abstractor implementations which additionally provide for abstraction from some details of the implemented specification. These subsume most formal notions of implementation in the literature. Both kinds of implementations satisfy a vertical composition and a (modified) horizontal composition property. All the definitions and results are shown to generalize to the framework of an arbitrary institution, and a way of changing institutions during the implementation process is introduced. All this is illustrated by means of simple concrete examples.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68P05 Data structures

Software:

ML
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Arbib, M.A., Manes, E.G.: Arrow, Structures and Functors: the Categorical Imperative. New York, London: Academic Press 1975 · Zbl 0374.18001
[2] Astesiano, E., Mascari, G.F., Reggio, G., Wirsing, M.: On the parameterized algebraic specification of concurrent systems. Proc. 10th Colloq. on Trees in Algebra and Programming, Joint Conf. on Theory and Practice of Software Development (TAPSOFT). Lect. Notes Comput. Sci. Vol. 185, pp. 342–358. Berlin, Heidelberg, New York: Springer 1985 · Zbl 0563.68018
[3] Astesiano, E., Reggio, G. : A unifying viewpoint for the constructive specification of cooperation, concurrency and distribution. Quaderni CNET no. 115, ETS Pisa (1983)
[4] Barwise, K.J.: Axioms for abstract model theory. Ann. Math. Log.7, 221–265 (1974) · Zbl 0324.02034
[5] Bauer, F.L., Broy, M., Dosch, W., Gnatz, R., Geiselbrechtinger, F., Hesse, W., Krieg-Brückner, B., Laut, A., Matzner, T., Möller, B., Partsch, H., Pepper, P., Samelson, K., Wirsing, M., Wössner, H.: Report on a wide spectrum language for program specification and development. Report TUM-I8104, Technische Univ. München (1981). See also: The Wide Spectrum Language CIP-L. Lect. Notes Comput. Sci. Vol. 183. Berlin, Heidelberg, New York: Springer 1985 · Zbl 0469.68003
[6] Bauer, F.L. Broy, M., Dosch, W., Gnatz, R., Krieg-Brückner, B., Laut, A., Luckmann, M., Matzner, T., Möller, B., Partsch, H., Papper, P., Samelson, K., Steinbrüggen, R., Wirsing, M., Wössner, H.: Programming in a wide spectrum language: a collection of examples. Sci. Comput. Prog.1, 73–114 (1981) · Zbl 0469.68003
[7] Bergstra, J.A., Meyer, J.J.: I/O computable data structures. SIGPLAN Notices16, 27–32 (1981)
[8] Bernot, G., Bidoit, M., Choppy, C.: Abstract implementations and correctness proofs. Proc. Symp. on Theoretical Aspects of Computer Science, Saarbrücken. Lect. Notes Comput. Sci. Vol. 210, pp. 236–251. Berlin, Heidelberg, New York: Springer 1986 · Zbl 0585.68025
[9] Bloom, S.L., Wagner, E.G.: Many-sorted theories and their algebras with some applications to data types. In: Algebraic Methods in Semantics. Nivat, M., Reynolds, J.C. (eds.), pp. 133–168. Cambridge: University Press 1985 · Zbl 0575.18004
[10] Broy, M., Möller, B., Pepper, P., Wirsing, M.: Algebraic implementations preserve program correctness. Sci. Comput. Prog.7, 35–53 (1986) · Zbl 0597.68021
[11] Broy, M., Wirsing, M.: Partial abstract types. Acta Inf.18, 47–64 (1982) · Zbl 0494.68020
[12] Burmeister, P.: A Model Theoretic Approach to Partial Algebras. Berlin: Akademie-Verlag 1986 · Zbl 0598.08004
[13] Burstall, R.M., Goguen, J.A. : Putting together theories to make specifications. Proc. 5th Intl. Joint Conf. on Artificial Intelligence, pp. 1045–1058. Cambridge 1977
[14] Burstall, R.M., Goguen, J.A.: The semantics of Clear, a specification language. Proc. of Advanced Course on Abstract Software Specifications, Copenhagen. Lect. Notes Comput. Sci. Vol. 86, pp. 292–332. Berlin, Heidelberg, New York: Springer 1980 · Zbl 0456.68024
[15] Burstall, R.M., Goguen, J.A. : Algebras, theories and freeness: an introduction for computer scientists. Proc. 1981 Marktoberdorf NATO Summer School. Reidel (1982) · Zbl 0518.68009
[16] Burstall, R.M., MacQueen, D.B., Sannella, D.T.: HOPE: an experimental applicative language. Proc. 1980 LISP Conference, pp. 136–143. Stanford 1980
[17] Dubois, E., Levy, N., Souquieres, J.: Formalising restructuring operators in a specification process. Proc. ESEC’87, Strasbourg 1987
[18] de Nicola, R., Hennessy, M.C.B.: Testing equivalences for processes. Theor. Comput. Sci.34, 83–133 (1984) · Zbl 0985.68518
[19] Ehrich, H.-D.: On realization and implementation. Proc. 10th Intl. Symp. on Mathematical Foundations of Computer Science, Strbske Pleso, Czechoslovakia. Lect. Notes Comput. Sci. Vol. 118, pp. 271–280. Berlin, Heidelberg, New York: Springer 1981 · Zbl 0465.68005
[20] Ehrich, H.-D.: On the theory of specification, implementation, and parametrization of abstract data types. J. Assoc. Comput. Mach.29, 206–227 (1982) · Zbl 0478.68020
[21] Ehrig, H., Fey, W., Hansen, H.: ACT ONE: an algebraic specification language with two levels of semantics. Report Nr. 83-03, Institut für Software und Theoretische Informatik, Technische Univ. Berlin 1983 · Zbl 0549.68010
[22] Ehrig, H., Kreowski, H.-J.: Parameter passing commutes with implementation of parameterized data types. Proc. 9th Intl. Colloq. on Automata, Languages and Programming, Aarhus, Denmark. Lect. Notes Comput. Sci. Vol. 140, pp. 197–211. Berlin, Heidelberg, New York: Springer 1982 · Zbl 0486.68016
[23] Ehrig, H., Kreowski, H.-J., Mahr, B., Padawitz, P.: Algebraic implementation of abstract data types. Theor. Comput. Sci.20, 209–263 (1982) · Zbl 0483.68018
[24] 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, Noordwijkerhout, Netherlands. Lect. Notes Comput. Sci. Vol. 85, pp. 157–168. Berlin, Heidelberg, New York: Springer 1980 · Zbl 0456.68101
[25] Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification I: Equations and Initial Semantics. EATCS Monographs on Theoretical Computer Science. Berlin, Heidelberg, New York: Springer 1985 · Zbl 0557.68013
[26] Ehrig, H., Thatcher, J.W., Lucas, P., Zilles, S.N. : Denotational and initial algebra semantics of the algebraic specification language LOOK. Draft report, IBM research 1982
[27] Ehrig, H., Wagner, E.G., Thatcher, J.W.: Algebraic specifications with generating constraints. Proc. 10th Intl. Colloq. on Automata, Languages and Programming, Barcelona. Lect. Notes Comput. Sci. Vol. 154, pp. 188–202. Berlin, Heidelberg, New York: Springer 1983 · Zbl 0518.68019
[28] Futatsugi, K., Goguen, J.A., Jouannaud, J.-P., Meseguer, J.: Principles of OBJ2. Proc. 12th ACM Symp. on Principles of Programming Languages, pp. 52–66. New Orleans 1985
[29] Ganzinger, H.: Parameterized specifications: parameter passing and implementation with respect to observability. Trans. Prog. Lang. Syst.5, 318–354 (1983) · Zbl 0511.68010
[30] Giarratana, V., Gimona, F., Montanari, U.: Observability concepts in abstract data type specification. Proc. 5th Intl. Symp. on Mathematical Foundations of Computer Science, Gdansk. Lect. Notes Comput. Sci. Vol. 45, pp. 576–587. Berlin, Heidelberg, New York: Springer 1976 · Zbl 0338.68023
[31] Gogolla, M.: Algebraic specifications with partially ordered sorts and declarations. Fb. 169, Abteilung Informatik, UniversitÄt Dortmund 1983
[32] Gogolla, M., Drosten, K., Lipeck, U., Ehrich, H.-D.: Algebraic and operational semantics of specifications allowing exceptions and errors. Theor. Comput. Sci.34, 289–313 (1984) · Zbl 0553.68012
[33] Goguen, J.A., Burstall, R.M. : CAT, a system for the structured elaboration of correct programs from structured specifications. Technical report CSL-118, SRI International, 1980 · Zbl 0456.68024
[34] Goguen, J.A., Burstall, R.M.: Introducing institutions. Proc. Logics of Programming Workshop. Clarke, E., Kozen, D. (eds.), Carnegie-Mellon University. Lect. Notes Comput. Sci. Vol. 164, pp. 221–256. Berlin, Heidelberg, New York: Springer 1984 · Zbl 0543.68021
[35] Goguen, J.A., Burstall, R.M.: Some fundamental algebraic tools for the semantics of computation. Part 1: Comma categories, colimits, signatures and theories. Theor. Comput. Sci.31, 175–210 (1984) · Zbl 0566.68065
[36] Goguen, J.A., Burstall, R.M.: A study in the foundations of programming methodology: specifications, institutions, charters and parchments. Proc. Workshop on Category Theory and Computer Programming, Guildford. Lect. Notes Comput. Sci. Vol. 240, pp. 313–333. Berlin, Heidelberg, New York: Springer 1986 · Zbl 0615.68002
[37] Goguen, J.A., Jouannaud, J.-P., Meseguer, J.: Operational semantics for order-sorted algebra. Proc. 12th Intl. Colloq. on Automata, Languages and Programming, Nafplion, Greece. Lect. Notes Comput. Sci. Vol. 194, pp. 221–231. Berlin, Heidelberg, New York: Springer 1985 · Zbl 0591.68041
[38] Goguen, J.A., Meseguer, J.: Universal realization, persistent interconnection and implementation of abstract modules. Proc. 9th Intl. Colloq. on Automata, Languages and Programming, Aarhus. Lect. Notes Comput. Sci. Vol. 140, pp. 265–281. Berlin, Heidelberg, New York: Springer 1982 · Zbl 0493.68014
[39] Goguen, J.A., Thatcher, J.W., Wagner, E.G.: An initial algebra approach to the specification, correctness, and implementation of abstract data types. IBM research report RC6487 (1976). Also in: Current Trends in Programming Methodology, Vol.4: Data Structuring. Yeh, R.T. (ed.), pp. 80–149. Englewood Cliffs, NJ: Prentice-Hall 1978
[40] Goguen, J.A., Thatcher, J.W., Wagner, E.G., Wright, J.B.: Initial algebra semantics and continuous algebras. J. Assoc. Comput. Mach.24, 68–95 (1977) · Zbl 0359.68018
[41] Gordon, M.J.: Denotational descriptions of Programming Languages. Berlin, Heidelberg, New York: Springer 1979 · Zbl 0412.68004
[42] Guttag, J.V.: The specification and application to programming of abstract data types. Ph.D. thesis, University of Toronto 1975
[43] Guttag, J.V., Horning, J.J.: Preliminary report on the Larch Shared Language. Report CSL-83-6, Computer Science Laboratory, Xerox PARC, 1983 · Zbl 0581.68007
[44] Kamin, S.: Final data types and their specification. Trans. Prog. Lang. Syst.5, 97–121 (1983) · Zbl 0498.68008
[45] Larsen, K.: Context-dependent bisimulation between processes. Ph.D. thesis, Dept. of Computer Science, University of Edinburgh, 1986
[46] Lipeck, U.: Ein algebraischer Kalkül für einer strukturierten Entwurf von Datenabstraktionen. Ph.D. thesis, Abteilung Informatik, UniversitÄt Dortmund 1983 · Zbl 0519.68020
[47] Liskov, B.H., Berzins, V.: An appraisal of program specifications. Computation Structures Group memo 141–1, Laboratory for Computer Science, MIT, 1977
[48] MacLane, S.: Categories for the Working Mathematician. Berlin, Heidelberg, New York: Springer 1971 · Zbl 0705.18001
[49] MacQueen, D.B.: Modules for Standard ML. Polymorphism2, 2 (1985). See also: Proc. 1984 ACM Symp. on LISP and Functional Programming, pp. 198–207. Austin, Texas, 1984
[50] Manna, Z., Waldinger, R.: A deductive approach to program synthesis. ACM Trans. Prog. Lang. Syst.2, 92–121 (1980) · Zbl 0468.68009
[51] Meseguer, J., Goguen, J.A.: Initiality, induction and computability. In: Algebraic Methods in Semantics. Nivat, M, Reynolds, J. (eds.), pp. 459–541. Cambridge: Univ. Press 1983 · Zbl 0571.68004
[52] Milner, R.G.: A theory of type polymorphism in programming. J. Comput. Syst. Sci.17, 348–375 (1978) · Zbl 0388.68003
[53] Milner, R.G.: The Standard ML core language. Polymorphism2, 2 (1985). See also: A proposal for Standard ML. Proc. 1984 ACM Symp. on LISP and Functional Programming, pp. 184–197. Austin, Texas, 1984
[54] Moore, E.F.: Gedanken-experiments on sequential machines. In: Automata Studies. Shannon, C.E., McCarthy, J. (eds.), pp. 129–153. Princeton: University Press 1956
[55] Orejas, F.: Characterizing composability of abstract implementations. Proc. Intl. Conf. on Foundations of Computation Theory, Borgholm, Sweden. Lect. Notes Comput. Sci. Vol. 158, pp. 335–346. Berlin, Heidelberg, New York: Springer 1983 · Zbl 0569.68014
[56] Parisi-Presicce, F., Blum, E.K.: The semantics of shared submodules specifications. Proc. 10th Colloq. on Trees in Algebra and Programming, Joint Conf. on Theory and Practice of Software Development (TAPSOFT). Lect. Notes Comput. Sci. Vol. 185, pp. 359–373. Berlin, Heidelberg, New York: Springer 1985 · Zbl 0563.68014
[57] Pepper, P. : On the correctness of type transformations. Talk at 2nd Workshop on Theory and Applications of Abstract Data Types, Passau, 1983
[58] Plotkin, G.D.: LCF considered as a programming language. Theor. Comput. Sci.5, 223–255 (1977) · Zbl 0369.68006
[59] Reichel, H. : Behavioural equivalence – a unifying concept for initial and final specification methods. Proc. 3rd Hungarian Computer Science Conference, pp. 27–39. Budapest, 1981 · Zbl 0479.68017
[60] Sannella, D.T., Tarlecki, A.: Some thoughts on algebraic specification. Proc. 3rd Workshop on Theory and Applications of Abstract Data Types, Bremen. Informatik-Fachberichte Vol. 116, pp. 31–38. Berlin, Heidelberg, New York: Springer 1985 · Zbl 0584.68036
[61] Sannella, D.T., Tarlecki, A.: Program specification and development in Standard ML. Proc. 12th ACM Symp. on Principles of Programming Languages, pp. 67–77. New Orleans, 1985 · Zbl 0563.68017
[62] Sannella, D.T., Tarlecki, A.: Specifications in an arbitrary institution. Inf. Control.76 (1988). See also: Building specifications in an arbitrary institution, Proc. Intl. Symposium on Semantics of Data Types, Sophia-Antipolis. Lect. Notes Comput. Sci. Vol. 173, pp. 337–356. Berlin, Heidelberg, New York: Springer 1984 · Zbl 0552.68015
[63] Sannella, D.T., Tarlecki, A.: Extended ML: an institution-independent framework for formal program development. Proc. Workshop on Category Theory and Computer Programming, Guildford. Lect. Notes Comput. Sci. Vol. 240, pp. 364–389. Berlin, Heidelberg, New York: Springer 1986 · Zbl 0616.68015
[64] Sannella, D.T., Tarlecki, A.: On observational equivalence and algebraic specification. J. Comput. Syst. Sci.34, 150–178 (1987). Extended abstract in: Proc. 10th Colloq. on Trees in Algebra and Programming, Joint Conf. on Theory and Practice of Software Development (TAPSOFT). Lect. Notes Comput. Sci. Vol. 185, pp. 308–322. Berlin, Heidelberg, New York: Springer 1985 · Zbl 0619.68028
[65] Sannella, D.T., Tarlecki, A.: Toward formal development of programs from algebraic specifications: implementations revisited (extended abstract). Proc. 12th Colloq. on Trees in Algebra and Programming, Joint Conf. on Theory and Practice of Software Development (TAPSOFT), Pisa. Lect. Notes Comput. Sci. Vol. 249, pp. 96–110. Berlin, Heidelberg, New York: Springer 1987 · Zbl 0614.68013
[66] Sannella, D.T., Wirsing, M.: Implementation of parameterised specifications. Report CSR-103-82, Dept. of Computer Science, Univ. of Edinburgh. Extended abstract in: Proc. 9th Intl. Colloq. on Automata, Languages and Programming, Aarhus. Lect. Notes Comput. Sci. Vol. 140, pp. 473–488. Berlin, Heidelberg, New York: Springer 1982 · Zbl 0492.68023
[67] Sannella, D.T., Wirsing, M.: A kernel language for algebraic specification and implementation. Report CSR-131-83, Dept. of Computer Science, Univ. of Edinburgh. Extended abstract in: Proc. Intl. Conf. on Foundations of Computation Theory, Borgholm, Sweden. Lect. Notes Comput. Sci. Vol. 158, pp. 413–427. Berlin, Heidelberg, New York: Springer 1983 · Zbl 0517.68043
[68] Schoett, O.: Data abstraction and the correctness of modular programming. Ph.D. thesis, University of Edinburgh, 1986
[69] Tarlecki, A.: On the existence of free models in abstract algebraic institutions. Theor. Comput. Sci.37, 269–304 (1985) · Zbl 0608.68014
[70] Tarlecki, A.: Quasi-varieties in abstract algebraic institutions. J. Comput. Syst. Sci.33, 333–360 (1986) · Zbl 0622.68033
[71] Tarlecki, A.: Software-system development – an abstract view. Proc. 10th IFIP World Computer Congress, Dublin, pp. 685–688. Amsterdam: North-Holland 1986
[72] Tarlecki, A., Wirsing, M.: Continuous abstract data types. Fundamenta Informaticae9, pp. 95–126 (1986). Extended abstract: Continuous abstract data types – basic machinery and results. Proc. Intl. Conf. on Fundamentals of Computation Theory, Cottbus, GDR. Lect. Notes Comput. Sci. Vol. 199, pp. 431–441. Berlin, Heidelberg, New York: Springer 1985 · Zbl 0571.68014
[73] Wand, M.: Specifications, models, and implementations of data abstractions. Theor. Comput. Sci.20, 3–32 (1982) · Zbl 0478.68021
[74] Wirsing, M.: Structured algebraic specifications: a kernel language. Theor. Comput. Sci.42, 123–249 (1986) · Zbl 0599.68021
[75] Zilles, S.N.: Algebraic specification of data types. Computation Structures Group memo 119, Laboratory for Computer Science, MIT (1974)
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.