×

On the correctness of modular systems. (English) Zbl 0874.68065

Summary: In modular software design it is expected that the correctness of the implementation of a complete system will be a consequence of the correctness of each module. Very often, this property has been associated to the satisfaction of the so-called horizontal and vertical composition properties, both at the specification and at the programming language levels. We introduce an abstract framework that allows us to represent, as specific instances, most concrete modular fameworks. In particular, the framework presented is “parametrized” by the specification and programming language formalisms, by the semantic constructs associated to modules and by the behavioural equivalence relation used to define module refinement. In addition, the framework is powerful enough to integrate specification and program design by allowing us to deal with incompletely specified systems. In this context, it is shown that, to achieve modular correctness, it is sufficient that the programming language satisfies the property of “stability”, as defined by Schoett, with respect to the given behavioural equivalence relation. In particular, modular correctness is shown to be independent of the satisfaction (or not) of the horizontal and vertical composition properties at the specification level. Finally, it is shown that the property of stability is just a compact formulation of the properties of horizontal and vertical composition at the programming language level.

MSC:

68N99 Theory of software
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Astesiao, E.; Cerioli, M., Relationships between logical frameworks, (Recent Trends in Data Type Specification. Recent Trends in Data Type Specification, Lecture Notes in Computer Science, Vol. 655 (1993), Springer: Springer Berlin)
[2] Bernot, G.; Bidoit, M., Proving the correctness of algebraically specified software: Modularity and observability issues, (Report LIENS-91-8 (1991), Dept. de Mathematiques et Informatique, Ecole Normale Superieur: Dept. de Mathematiques et Informatique, Ecole Normale Superieur Paris)
[3] Bidoit, M.; Hennicker, R., A general framework for modular implementations of modular system specifications, (Proc. TAPSOFT 93. Proc. TAPSOFT 93, Orsay, France. Proc. TAPSOFT 93. Proc. TAPSOFT 93, Orsay, France, Lecture Notes in Computer Science, Vol. 668 (1993), Springer: Springer Berlin), 199-214 · Zbl 1497.68288
[4] Blum, E. K.; Ehrig, H.; Parisi-Presicce, F., Algebraic specification of modules and their basic interconnections, J. Comput. System Sci., 34, 293-339 (1987) · Zbl 0619.68027
[5] Burstall, R. M.; Goguen, J. A., The semantics of Clear, a specification language, (Proc. Copenhagen Winter School on Abstract Software Specification. Proc. Copenhagen Winter School on Abstract Software Specification, Lecture Notes in Computer Science, Vol. 86 (1980), Springer: Springer Berlin), 292-332 · Zbl 0456.68024
[6] Clérici, S.; Orejas, F., GSBL: an algebraic specification language based on inheritance, (Proc. 1988 European Conf. on Object Oriented Programming. Proc. 1988 European Conf. on Object Oriented Programming, Oslo. Proc. 1988 European Conf. on Object Oriented Programming. Proc. 1988 European Conf. on Object Oriented Programming, Oslo, Lecture Notes in Computer Science, Vol. 322 (1988), Springer: Springer Berlin), 78-92
[7] Diaconescu, R.; Goguen, J. A.; Stefaneas, P., Logical support for modularisation, (Report Prog. Res. Group (1991), Oxford Univ)
[8] 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
[9] Ehrig, H.; Mahr, B., Fundamentals of Algebraic Specifications 1 (1985), Springer: Springer Berlin · Zbl 0557.68013
[10] Ehrig, H.; Mahr, B., Fundamentals of Algebraic Specifications 2 (1990), Springer: Springer Berlin · Zbl 0759.68013
[11] Ehrig, H.; Orejas, F.; Cornelius, F.; Baldamus, M., Abstract and behaviour module specifications, (Report 93-25 (1993), Tech. Univ: Tech. Univ Berlin) · Zbl 0923.68089
[12] Ehrig, H.; Parisi-Presicce, F., Algebraic specification graph-grammars: a junction between module specifications and graph grammars, (Ehrig, H.; Kreowski, H.-J.; Rozenberg, G., Graph-Grammars and their Application to Computer Science. Graph-Grammars and their Application to Computer Science, Lecture Notes in Computer Science, Vol. 532 (1991), Springer: Springer Berlin), 292-310 · Zbl 0765.68087
[13] Ehrig, H.; Pepper, P.; Orejas, F., On recent trends in algebraic specification, (Proc. ICALP ’89. Proc. ICALP ’89, Lecture Notes in Computer Science, Vol. 372 (1989), Springer: Springer Berlin), 263-288 · Zbl 0689.68013
[14] Goguen, J. A.; Burstall, R. M., CAT, a system for the structured elaboration of correct programs from structured specifications, (Technicl Report CSL-118 (1980), Computer Science Laboratory, SRI International) · Zbl 0456.68024
[15] Goguen, J. A.; Burstall, R. M., Introducing institutions, (Proc. Logics of Programming Workshop, Carnegie-Mellon. Proc. Logics of Programming Workshop, Carnegie-Mellon, Lecture Notes in Computer Science, Vol. 164 (1984), Springer: Springer Berlin), 221-256 · Zbl 1288.03001
[16] Goguen, J. A.; Burstall, R. M., Institutions: abstract model theory for specification and programming, J. ACM, 39, 95-146 (1992) · Zbl 0799.68134
[17] Goguen, J. A.; Meseguer, J., Universal realization, persistent interconnection and implementation of abstract modules, (Proc. 9th Internat. Coll. on Automata, Languages and Programming. Proc. 9th Internat. Coll. on Automata, Languages and Programming, Aarhus. Proc. 9th Internat. Coll. on Automata, Languages and Programming. Proc. 9th Internat. Coll. on Automata, Languages and Programming, Aarhus, Lecture Notes in Computer Science, Vol. 140 (1982), Springer: Springer Berlin), 265-281 · Zbl 0493.68014
[18] Hoare, C. A.R., Proofs of correctness of data representations, Acta Inform., 1, 271-281 (1972) · Zbl 0244.68009
[19] Meseguer, J., General logics, (Proc. Logic. Coll. ’87. Proc. Logic. Coll. ’87, Granada (1989), North-Holland: North-Holland Amsterdam) · Zbl 0691.03001
[20] Nivela, P., Semántica de comportamiento para especificaciones algebraicas, (Ph.D. Thesis (1987), Universitat Politècnica de Catalunya: Universitat Politècnica de Catalunya Barcelona)
[21] Nivela, P.; Orejas, F., Initial behavioural semantics for algebraic specifications, (Recent Trends in Data Type Specification, Selected Papers from the 5th Workshop on Specification of Abstract Data Types. Recent Trends in Data Type Specification, Selected Papers from the 5th Workshop on Specification of Abstract Data Types, Gullane, Scotland. Recent Trends in Data Type Specification, Selected Papers from the 5th Workshop on Specification of Abstract Data Types. Recent Trends in Data Type Specification, Selected Papers from the 5th Workshop on Specification of Abstract Data Types, Gullane, Scotland, Lecture Notes in Computer Science, Vol. 332 (1988), Springer: Springer Berlin), 184-207 · Zbl 0679.68026
[22] Orejas, F.; Navarro, M.; Sánchez, A., Implementations and behavioural equivalence: a survey, (Invited Lecture, 8th Workshop on Specification of Abstract Data Types Dourdan. Invited Lecture, 8th Workshop on Specification of Abstract Data Types Dourdan, 1991. Invited Lecture, 8th Workshop on Specification of Abstract Data Types Dourdan. Invited Lecture, 8th Workshop on Specification of Abstract Data Types Dourdan, 1991, Lecture Notes in Computer Science, Vol. 655 (1993), Springer: Springer Berlin), 93-125
[23] Orejas, F.; Nivela, P.; Ehrig, H., Semantical constructions for categories of behavioural specifications, (Proc. Workshop on Categorical Methods in Computer Science with Aspects from Topology. Proc. Workshop on Categorical Methods in Computer Science with Aspects from Topology, Lecture Notes in Computer Science, Vol. 393 (1989), Springer: Springer Berlin), 220-241
[24] Orejas, F.; Sacristan, V.; Clérici, S., Development of algebraic specifications with constraints, (Proc. Workshop on Categorical Methods in Computer Science with Aspects from Topology. Proc. Workshop on Categorical Methods in Computer Science with Aspects from Topology, Lecture Notes in Computer Science, Vol. 393 (1989), Springer: Springer Berlin), 102-123
[25] Reichel, H., Initially restricting algebraic theories, (Proc. MFCS 80. Proc. MFCS 80, Lecture Notes in Computer Science, Vol. 88 (1980), Springer: Springer Berlin), 504-514 · Zbl 0469.68026
[26] Reichel, H., Behavioural equivalence — a unifying concept for initial and final specification methods, (Proc. 3rd Hungarian Comput. Sci. Conf. (1981)), 27-39 · Zbl 0479.68017
[27] Sannella, D. T.; Tarlecki, A., On observational equivalence and algebraic specification, J. Comput. System Sci., 34, 150-178 (1987) · Zbl 0619.68028
[28] Sannella, D. T.; Tarlecki, A., Acta Inform., 25, 233-281 (1988), full version in · Zbl 0621.68004
[29] Sannella, D. T.; Tarlecki, A., Specifications in an arbitrary institution, Inform. and Comput., 76, 165-210 (1988) · Zbl 0654.68017
[30] Sannella, D. T.; Tarlecki, A., Toward formal development of ML programs: foundations and methodology, (Proc. Tapsoft ’89. Proc. Tapsoft ’89, Barcelona. Proc. Tapsoft ’89. Proc. Tapsoft ’89, Barcelona, Lecture Notes in Computer Science, Vol. 352 (1989), Springer: Springer Berlin), 375-389
[31] Schoett, O., Report CST-42-87, (Data abstraction and the correctness of modular programming. Data abstraction and the correctness of modular programming, Ph.D. Thesis (1987), Dept. of Computer Science, Univ. of Edinburgh)
[32] Wirsing, M., Algebraic Specification, (Handbook of Theoretical Computer Science, Vol. 2: Formal Models and Semantics (1991), Elsevier: Elsevier Amsterdam), 675-788 · Zbl 0900.68309
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.