×

zbMATH — the first resource for mathematics

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
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Astesiao, E.; Cerioli, M., Relationships between logical frameworks, ()
[2] Bernot, G.; Bidoit, M., Proving the correctness of algebraically specified software: modularity and observability issues, ()
[3] Bidoit, M.; Hennicker, R., A general framework for modular implementations of modular system specifications, (), 199-214
[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, (), 292-332 · Zbl 0456.68024
[6] Clérici, S.; Orejas, F., GSBL: an algebraic specification language based on inheritance, (), 78-92
[7] Diaconescu, R.; Goguen, J.A.; Stefaneas, P., Logical support for modularisation, ()
[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 Berlin · Zbl 0557.68013
[10] Ehrig, H.; Mahr, B., Fundamentals of algebraic specifications 2, (1990), Springer Berlin · Zbl 0759.68013
[11] Ehrig, H.; Orejas, F.; Cornelius, F.; Baldamus, M., Abstract and behaviour module specifications, () · Zbl 0923.68089
[12] Ehrig, H.; Parisi-Presicce, F., Algebraic specification graph-grammars: a junction between module specifications and graph grammars, (), 292-310 · Zbl 0765.68087
[13] Ehrig, H.; Pepper, P.; Orejas, F., On recent trends in algebraic specification, (), 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, () · Zbl 0456.68024
[15] Goguen, J.A.; Burstall, R.M., Introducing institutions, (), 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, (), 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, () · Zbl 0691.03001
[20] Nivela, P., Semántica de comportamiento para especificaciones algebraicas, ()
[21] Nivela, P.; Orejas, F., Initial behavioural semantics for algebraic specifications, (), 184-207 · Zbl 0679.68026
[22] Orejas, F.; Navarro, M.; Sánchez, A., Implementations and behavioural equivalence: a survey, (), 93-125
[23] Orejas, F.; Nivela, P.; Ehrig, H., Semantical constructions for categories of behavioural specifications, (), 220-241
[24] Orejas, F.; Sacristan, V.; Clérici, S., Development of algebraic specifications with constraints, (), 102-123
[25] Reichel, H., Initially restricting algebraic theories, (), 504-514 · Zbl 0469.68026
[26] Reichel, H., Behavioural equivalence — a unifying concept for initial and final specification methods, (), 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.; Sannella, D.T.; Tarlecki, A., Toward formal development of programs from algebraic specifications: implementations revisited, extended abstract, (), 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, (), 375-389
[31] Schoett, O., Report CST-42-87, ()
[32] Wirsing, M., Algebraic specification, (), 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. 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.