×

zbMATH — the first resource for mathematics

Essential concepts of algebraic specification and program development. (English) Zbl 0887.68070
Summary: The main ideas underlying work on the model-theoretic foundations of algebraic specification and formal program development are presented in an informal way. An attempt is made to offer an overall view, rather than new results, and to focus on the basic motivation behind the technicalities presented elsewhere.

MSC:
68Q65 Abstract data types; algebraic specification
Software:
LARCH; ML; OBJ3
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Astesiano, E. and Reggio, G.: Formally-driven friendly specifications of concurrent systems: a two-rail approach.Proc. ICSE-17 Workshop on Formal Methods Application in Software Engineering Practice, Seattle, 158-165 (1995).
[2] Barwise, J.: Axioms for abstract model theory.Ann. Math. Logic 7:221-265 (1974). · Zbl 0324.02034 · doi:10.1016/0003-4843(74)90016-3
[3] Barwise, J. and Feferman, E.: (eds.)Model-Theoretic Logics. Springer (1985). · Zbl 0587.03001
[4] Bauer, F. and Wössner, H.:Algorithmic Language and Program Development. Springer (1982).
[5] Beierle, C. and Voß, A.: Viewing implementations as an institution.Proc. 1987 Conference on Category Theory and Computer Science, Edinburgh. Springer LNCS 283, 196-218 (1987). · Zbl 0639.68025
[6] Bidoit, M., Gaudel, M.-C. and Mauboussin, A.: How to make algebraic specifications more understandable? An experiment with the PLUSS specification language.Science of Computer Programming 12:1-38 (1989). · Zbl 0678.68011 · doi:10.1016/0167-6423(89)90026-9
[7] Bidoit, M, Hennicker, R. and Wirsing, M.: Behavioural and abstractor specifications.Science of Computer Programming 25:149-186 (1995). · Zbl 0853.68130 · doi:10.1016/0167-6423(95)00014-3
[8] Bidoit, M., Kreowski, H.-J., Lescanne, P., Orejas, F. and Sannella, D.: (eds.)Algebraic System Specification and Development: A Survey and Annotated Bibliography. Springer LNCS 501 (1991). · Zbl 0875.68642
[9] Biswas, S.: Higher-order functors with transparent signatures.Proc. 22nd ACM Symp. on Principles of Programming Languages, San Francisco, 154-163 (1995).
[10] Burstall, R. and Goguen, J.: Putting theories together to make specifications.Proc. 5th Intl. Joint Conf. on Artificial Intelligence, Cambridge, Massachusetts, 1045-1058 (1977).
[11] Burstall, R. and Goguen, J.: The semantics of Clear, a specification language.Proc. 1979 Copenhagen Winter School on Abstract Software Specification. Springer LNCS 86, 292-332 (1980). · Zbl 0456.68024
[12] Cengarle, M.V.: Formal specifications with higher-order parameterization. Ph.D. thesis, LMU München (1994). · Zbl 0921.68058
[13] Davis, A.:Software Requirements: Analysis and Specification. Prentice Hall (1990).
[14] De Nicola, R. and Hennessy, M.: Testing equivalences for processes.Theoretical Computer Science 34:83-133 (1984). · Zbl 0985.68518 · doi:10.1016/0304-3975(84)90113-0
[15] Diaconescu, R., Goguen, J. and Stefaneas, P.: Logical support for modularization. In:Logical Environments (G. Huet and G. Plotkin, eds.). Cambridge Univ. Press, 83-130 (1993).
[16] Ehrig, H., Baldamus, M. and Orejas, F.: New concepts of amalgamation and extension of a general theory of specifications.Selected Papers from the 8th Workshop on Specification of Abstract Data Types, Dourdan. Springer LNCS 655, 199-221 (1993).
[17] Ehrig, H., Kreowski, H.-J., Mahr, B. and Padawitz, P.: Algebraic implementation of abstract data types.Theoretical Computer Science 20:209-263 (1982). · Zbl 0483.68018 · doi:10.1016/S0304-3975(82)80001-7
[18] Ehrig, H. and Mahr, B.:Fundamentals of Algebraic Specification I: Equations and Initial Semantics. Springer (1985). · Zbl 0557.68013
[19] Farrés-Casals, J.: Verification in ASL and Related Specification Languages. Ph.D. thesis, report CST-92-92, Dept. of Computer Science, Univ. of Edinburgh (1992).
[20] Fiadeiro, J. and Sernadas, A.: Structuring theories on consequence.Selected Papers from the 5th Workshop on Specification of Abstract Data Types, Gullane. Springer LNCS 332, 44-72 (1988).
[21] Fitzgerald, J. and Jones, C.: Modularizing the formal description of a database system.Proc. VDM’90 Conference, Kiel. Springer LNCS 428, 198-210 (1990).
[22] Goguen, J.: Parameterized programming.IEEE Trans. on Software Engineering SE-10(5):528-543 (1984). · Zbl 0545.68017 · doi:10.1109/TSE.1984.5010277
[23] Goguen, J. and Burstall, R.: CAT, a system for the structured elaboration of correct programs from structured specifications. Technical report CSL-118, SRI International (1980). · Zbl 0456.68024
[24] Goguen, J., and Burstall, R.: Introducing institutions.Proc. Logics of Programming Workshop, Carnegie-Mellon. Springer LNCS 164, 221-256 (1984). · Zbl 0543.68021
[25] Goguen, J. and Burstall, R.: Institutions: abstract model theory for specification and programming.Journal of the Assoc. for Computing Machinery 39:95-146 (1992). · Zbl 0799.68134
[26] Goguen, J. and Luqi.: Formal methods and social context in software development.Proc. 6th Joint Conf. on Theory and Practice of Software Development, TAPSOFT’95, Aarhus. Springer LNCS 915, 62-81 (1995).
[27] Goguen, J. and Meseguer, J.: Universal realization, persistent interconnection and implementation of abstract modules.Proc. Intl. Colloq. on Automata, Languages and Programming, Aarhus. Springer LNCS 140, 265-281 (1982). · Zbl 0493.68014
[28] Goguen, J. and Meseguer, J.: Completeness of many-sorted equational logic.Houston Journal of Mathematics 11(3):307-334 (1985). · Zbl 0602.08004
[29] Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K. and Jouannaud, J.-P.: Introducing OBJ3. Techical Report SRI-CSL-92-03, SRI International (1992).
[30] Guttag, J. and Horning, J.: Formal specification as a design tool.Proc. 7th ACM Symp. on Principles of Programming Languages, Las Vegas, 251-261 (1980).
[31] Guttag, J. and Horning, J.:Larch: Languages and Tools for Formal Specification. Springer (1993). · Zbl 0794.68103
[32] Guttag, J., Horning, J. and Wing, J.: Some notes on putting formal specifications to productive use.Science of Computer Programming 2:53-68 (1982). · Zbl 0491.68012 · doi:10.1016/0167-6423(82)90004-1
[33] Harper, R., Sannella, D. and Tarlecki, A.: Structured theory presentations and logic representations.Annals of Pure and Applied Logic 67:113-160 (1994). · Zbl 0809.03019 · doi:10.1016/0168-0072(94)90009-4
[34] Hayes, I.J. and Jones, C.B.: Specifications are not (necessarily) executable.Software Engineering Journal 4(6):320-338 (1989). · doi:10.1049/sej.1989.0045
[35] Hoare, C.A.R.: Proofs of correctness of data representations.Acta Informatica 1:271-281 (1972). · Zbl 0244.68009 · doi:10.1007/BF00289507
[36] Hoffmann, B. and Krieg-Brückner, B.: (eds.)PROgram Development by SPECification and TRAnsformation: Methodology ? Language Family ? System. Springer LNCS 680 (1993). · Zbl 0825.00088
[37] Hofmann, M. and Sannella, D.: On behavioural abstraction and behavioural satisfaction in higher-order logic.Theoretical Computer Science 167:3-45 (1996). · Zbl 0874.68196 · doi:10.1016/0304-3975(96)00068-0
[38] Hußmann, H.: Rapid prototyping for algebraic specifications: RAP system user’s manual. Report MIP-8504, Universität Passau (1985).
[39] Jones, C:Systematic Software Development using VDM. Prentice Hall (1986). · Zbl 0584.68008
[40] Kahrs, S, Sannella, D. and Tarlecki, A.: The definition of Extended ML. Report ECS-LFCS-94-300, Dept. of Computer Science, Univ. of Edinburgh (1994). · Zbl 0813.68132
[41] Kahrs, S, Sannella, D. and Tarlecki, A.: The definition of Extended ML: a gentle introduction.Theoretical Computer Science 173, to appear (1997). · Zbl 0901.68024
[42] Kazmierczak, E.: Modularizing the specification of a small database system in Extended ML.Formal Aspects of Computing 4:100-142 (1992). · Zbl 0739.68031 · doi:10.1007/BF01214958
[43] Krieg-Brückner, B. and Sannella, D.: Structuring specifications in-the-large and in-the-small: higher-order functions, dependent types and inheritance in SPECTRAL.Proc. 4th Joint Conf. on Theory and Practice of Software Development, TAPSOFT’91, Brighton. Springer LNCS 494, 313-336 (1991).
[44] Li, W.: A logical framework for evolution of specifications.Proc. 5th European Symp. on Programming, Edinburgh. Springer LNCS 788, 394-408 (1994).
[45] MacQueen, D. and Tofte, M.: A semantics for higher-order functors.Proc. 5th European Symp. on Programming, Edinburgh. Springer LNCS 788, 409-423 (1994).
[46] Milner, R., Tofte, M. and Harper, R.:The Definition of Standard ML. MIT Press (1990).
[47] Morris, J. and Ahmed, S.: Designing and refining specifications with modules.Proc. 3rd Refinement Workshop, Hursley Park, 1990. Springer Workshops in Computing, 73-95 (1991).
[48] Navarro, M., Orejas, R and Sanchez, A.: On the correctness of modular systems.Theoretical Computer Science 140:139-177 (1995). · Zbl 0874.68065 · doi:10.1016/0304-3975(94)00207-Y
[49] Nelson, G.: (ed.)System Programming with Modula-3. Prentice Hall (1991).
[50] Nivela, P. and Orejas, F.: Initial behaviour semantics for algebraic specifications.Selected Papers from the 5th Workshop on Specification of Abstract Data Types, Gullane. Springer LNCS 332, 184-207 (1988).
[51] Orejas, F.: Characterizing composability of abstract implementations.Proc. 1983 Intl. Conf. on Foundations of Computation Theory, Borgholm. Springer LNCS 158, 335-346 (1983). · Zbl 0569.68014
[52] Paulson, L.:ML for the Working Programmer. Cambridge Univ. Press (1991). · Zbl 0863.68032
[53] Reichel, H.: Behavioural equivalence ? a unifying concept for initial and final specification methods.Proc. 3rd Hungarian Computer Science Conference, 27-39 (1981). · Zbl 0479.68017
[54] Robertson, D., Agusti, J., Hesketh, J. and Levy, J.: Expressing program requirements using refinement lattices.Fundamenta Informaticae 21:163-183 (1994). · Zbl 0819.68077
[55] Sannella, D.: Formal program development in Extended ML for the working programmer.Proc. 3rd BCS/FACS Workshop on Refinement, Hursley Park. Springer Workshops in Computing, 99-130 (1991).
[56] Sannella, D. and Burstall, R.: Structured theories in LCF.Proc. Colloq. on Trees in Algebra and Programming, L’Aquila. Springer LNCS 159, 377-391 (1983). · Zbl 0527.68070
[57] Sannella, D., Sokolowski, S. and Tarlecki, A.: Toward formal development of programs from algebraic specifications: parameterization revisited.Acta Informatica 29:689-736 (1992). · Zbl 0790.68077 · doi:10.1007/BF01191893
[58] Sannella, D. and Tarlecki, A.: Extended ML: an institution-independent framework for formal program development.Proc. Intl. Workshop on Category Theory and Computer Programming, Guildford. Springer LNCS 240, 364-389 (1986). · Zbl 0616.68015
[59] Sannella, D. and Tarlecki, A.: On observational equivalence and algebraic specification.J. of Computer and System Sciences 34:150-178 (1987). · Zbl 0619.68028 · doi:10.1016/0022-0000(87)90023-7
[60] Sannella, D. and Tarlecki, A.: Specifications in an arbitrary institution.Information and Computation 76:165-210 (1988). · Zbl 0654.68017 · doi:10.1016/0890-5401(88)90008-9
[61] Sannella, D. and Tarlecki, A.: Toward formal development of programs from algebraic specifications: implementations revisited.Acta Informatica 25:233-281 (1988). · Zbl 0621.68004 · doi:10.1007/BF00283329
[62] Sannella, D. and Tarlecki, A.: Toward formal development of ML programs: foundations and methodology.Proc. 3rd Joint Conf. on Theory and Practice of Software Development, Barcelona. Springer LNCS 352, 375-389 (1989).
[63] Sannella, D. and Tarlecki, A.: Extended ML: past, present and future.Proc. 7th Intl. Workshop on Specification of Abstract Data Types, Wusterhausen. Springer LNCS 534, 297-322 (1991).
[64] Sannella, D. and Tarlecki, A.:Foundations of Algebraic Specifications and Formal Program Development. Cambridge Univ. Press, to appear (199?). · Zbl 1237.68129
[65] Sannella, D. and Wirsing, M.: Implementation of parameterized specifications.Proc. Intl. Colloq. on Automata, Languages and Programming, Aarhus. Springer LNCS 140, 473-488 (1982). · Zbl 0492.68023
[66] Sannella, D. and Wirsing, M.: A kernel language for algebraic specification and implementation.Proc. 1983 Intl. Conf. on Foundations of Computation Theory, Borgholm. Springer LNCS 158, 413-427 (1983). · Zbl 0517.68043
[67] Schoett, O.: Data Abstraction and the Correctness of Modular Programming. Ph.D. thesis, report CST-42-87, Dept. of Computer Science, Univ. of Edinburgh (1987).
[68] Schoett, O.: Two impossibility theorems on behavioural specification of abstract data types.Acta Informatica 29:595-621 (1992). · Zbl 0790.68080 · doi:10.1007/BF01185563
[69] Sommerville, I.:Software Engineering (4th edition). Addison-Wesley (1992). · Zbl 0679.68003
[70] Tofte, M.: Principle signatures for higher-order program modules.Proc. 19th ACM Symp. on Principles of Programming Languages, Albuquerque, 189-199 (1992).
[71] Wirsing, M.: Structured algebraic specifications: a kernel language.Theoretical Computer Science 42:123-249 (1986). · Zbl 0599.68021 · doi:10.1016/0304-3975(86)90051-4
[72] Wirsing, M.: Structured specifications: syntax, semantics and proof calculus.Logic and Algebra of Specification (F. Bauer, W. Brauer and H. Schwichtenberg, eds.). Springer, 411-442 (1993).
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.