Abstract
Given a requirements specification for a software system, a simple (modular) software development process can be represented by a tree, as follows: Here, the (informal or semi-formal) requirements specification is transformed into a detailed (formal) specification consisting of the specification modules M1,..., Mn. Then, the development phase starts and each of the specification modules is refined into a new set of modules. The process continues until all the specification modules describe objects that can be directly coded in the given programming language, obtaining as a result the set of program modules Pi1,..., Pik. Modular correctness means that the set of program modules Pi1,..., Pik should be a correct implementation of the given system if every refinement step applied to any module is correct.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bernot G, Bidoit M. Proving the correctness of Algebraically Specified Software: Modularity and Observability Issues. Report LIENS-91-8, D.M.L, Ecole Normale Supérieur, Paris (1991).
Burstall R, Goguen J. The semantics of Clear, a specification language, Proc. Copenhagen Winter School on Abstract Software Specification, Springer LNCS 86, pp. 292–332, 1980.
Bidoit M., Hennicker R. A general framework for modular implementations of modular system specifications, in Proc. TAPSOFT 93 (Orsay, France), Springer LNCS 668 (1993), 199–214.
Clérici S, Orejas F. GSBL: an algebraic specification language based on inheritance. Proc. 1988 Eur. Conf. on Object Oriented Prog. Springer LNCS 322, 78–92 (1988).
Diaconescu R, Goguen J, Stefaneas P. Logical support for modularisation, Report Prog. Res. Group, Oxford University, 1991.
Ehrig H, Baldamus M, Cornelius F, Orejas F. Theory of algebraic module specifications including behavioural semantics and constraints, Proc. AMAST 91.
Ehrig H, Mahr B. Fundamentals of Algebraic Specifications 1, Springer 1985.
Ehrig H, Mahr B. Fundamentals of Algebraic Specifications 2, Springer 1989.
Goguen J, Burstall R. CAT, a system for the structured elaboration of correct programs from structured specifications. Technical report CSL-118, Comp. Sc. Laboratory, SRI Int. (1980).
Goguen J, Burstall R. Institutions: Abstract model theory for specification and programming, Journ. of the ACM 39, 1 (1992) 95–146.
Goguen J, Meseguer J. Universal realization, persistent interconnection and implementation of abstract modules. Proc. 9th ICALP, Aarhus. Springer LNCS 140, 265–281 (1982).
Orejas F, Navarro M, Sánchez A. Implementations and behavioural equivalence: a survey.8th Workshop on Specification of Abstract Data Types. Springer LNCS 655 (1993), 93–125.
Orejas F, Sacristan V, Clérici S. Development of algebraic specifications with constraints, in ‘Categorical Methods in Computer Science’. Springer LNCS 393, 102–123 (1989).
Reichel H. Initially restricting algebraic theories, Proc. MFCS 80, Springer LNCS 88 (1980), pp. 504–514.
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).
Sannella DT, Tarlecki A. Toward formal development of programs from algebraic specifications: implementations revisited. Acta Informatica 25, 233–281 (1988).
Sannella DT, Tarlecki A. Toward formal development of ML programs: foundations and methodology. LFCS Report Series, Univ. of Edinburgh ECS-LFCS-89–71(1989).
Wirsing M. Algebraic Specification. Handbook of Theoretical Computer Science, Vol 2: Formal Models and Semantics, Elsevier (1991) 675–788.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1994 British Computer Society
About this paper
Cite this paper
Navarro, M., Orejas, F., Sánchez, A. (1994). On the Correctness of Modular Systems. In: Nivat, M., Rattray, C., Rus, T., Scollo, G. (eds) Algebraic Methodology and Software Technology (AMAST’93). Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3227-1_21
Download citation
DOI: https://doi.org/10.1007/978-1-4471-3227-1_21
Publisher Name: Springer, London
Print ISBN: 978-3-540-19852-9
Online ISBN: 978-1-4471-3227-1
eBook Packages: Springer Book Archive