Abstract
This paper is a first attempt at a formal foundation of specification languages allowing their basic modules to be defined in several formalisms. More precisely a rigorous notion of a compositional tool for importing/exporting specifications between two instances of one specification metalanguage on different basic algebraic frameworks is proposed.
Adopting the notion of institution as a synonym for formalism, we introduce and develop the concept of simulation of an institution by another. Then we deal with the simulation of basic and structured specifications, introducing the concept of simulation independent metalanguage, a generalization of institution independent languages, which allows “putting together theories from different formalisms to make specifications”. Since simulation generalizes the notion of implementation and allows relating implementations in different formalisms, a third dimension is added to the well known horizontal and vertical compositions of specifications, typical of Clear and ASL.
This work has been partially supported by Esprit-BRA W.G. n.6071 COMPASS, Progetto Finalizzato Sistemi Informatici e Calcolo Parallelo of C.N.R. (Italy), MURST-40% Modelli della computazione e dei linguaggi di programmazione
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
E. Astesiano and M. Cerioli. Relationships between logical frames. In Recent Trends in Data Type Specification,number 655 in Lecture Notes in Computer Science, pages 126–143, Berlin, 1993. Springer Verlag.
C. Beierle and A. Voss. Viewing implementations as an institution. In D. Pitt, A. Poigné, and D. Rydeheard, editors, Proceedings of Category Theory and Computer Science, number 283 in Lecture Notes in Computer Science, pages 196–218, Berlin, 1987. Springer Verlag.
R. Burstall and J. A. Goguen. Putting theories together to make specifications. In Proceedings of the 5th International Joint Conference on Artificial Intelligence, pages 1045–1058, Cambridge, 1977.
R. Burstall and J. A. Goguen. The semantics of clear, a specification language. In D. Bjorner, editor, Proceedings of the 1979 Copenhagen Winter School on Abstract Software Specification, number 86 in Lecture Notes in Computer Science, pages 292–332, Berlin, 1980. Springer Verlag.
M. Cerioli. Relationships between Logical Formalisms. PhD thesis, Universities of Pisa, Genova and Udine, 1993.
J. Goguen and R. Burstall. Introducing institutions. In E. Clarke and D. Kozen, editors, Logics of Programs Workshop, number 164 in Lecture Notes in Computer Science, pages 221–256, Berlin, 1984. Springer Verlag.
J. Goguen, J. Thatcher, and Wagner. An initial algebra approach to the specification, correctness, and implementation of abstract data types. In R. Yeh, editor, Current Trends in Programming Methodology, pages 80149. Prentice-Hall, 1976.
J. Goguen and T. Winkler. Introducing OBJ3. Technical Report SRICSL-88–9, Computer Science Lab., SRI International, 1988.
C. Hoare. Proof of correctness of data representation. Acta Informatica, 1: 271–281, 1972.
C. Jones. Systematic Software Development using VDM. Prentice Hall International, 1990.
V. Manca, A. Salibra, and G. Scollo. Equational type logic. Theoretical Computer Science,77:131–159, 1990. Special Issue dedicated to AMAST’89.
M. Navarro, P. Nivela, F. Orejas, and A. Sanchez. On translating partial to total specifications with applications to theorem proving for partial specifications. Technical Report LSI-89–21, Universitat Politecnica de Catalunya, 1990.
D. Parnas. A technique for software module specification. Communications of A.C.M., 15, 1972.
D. Sannella and A. Tarlecki. Specifications in an arbitrary institution. Information and Computation, 76: 165–210, 1988.
D. Sannella and M. Wirsing. A kernel language for algebraic specification and implementation. In M. Karpinski, editor, International Conference on Foundations of Computation, number 158 in Lecture Notes in Computer Science, pages 413–427, Berlin, 1983. Springer Verlag.
J. Spivey. The Z Notation: a Reference Manual. Prentice-Hall, New-York, 1989.
M. Wirsing. Algebraic specification. In Handbook of Theoretical Computer Science. North Holland, 1990.
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
Astesiano, E., Cerioli, M. (1994). Multiparadigm Specification Languages: a First Attempt at Foundations. In: Andrews, D.J., Groote, J.F., Middelburg, C.A. (eds) Semantics of Specification Languages (SoSL). Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3229-5_10
Download citation
DOI: https://doi.org/10.1007/978-1-4471-3229-5_10
Publisher Name: Springer, London
Print ISBN: 978-3-540-19854-3
Online ISBN: 978-1-4471-3229-5
eBook Packages: Springer Book Archive