Abstract
This paper presents a model inference system to control instantiation of generic modules. Generic parameters are specified by properties which represent classes of modules sharing some common features. Just as type checking consists in verifying that an expression is well typed, model checking allows to detect whether a (possibly generic) instantiation of a generic module is valid, i.e. whether the instantiation module is a model of the parameterizing property. Equality of instances can be derived from a canonical representation of modules. At last, we show how the code of generic modules can be shared for all instances of modules.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Reference Manual of the Programming Language Ada. ANSI/MIL-STD 1815A, 1983.
M. V. Aponte. Extending record typing to type parametric modules with sharing. In 20th Symposium on Principles of Programming Languages, 1993.
G. Bernot and M. Bidoit. Proving correctness of algebraically specified software: Modularity and observability issues. In Proceedings of AMAST'91. Springer-Verlag, 1991.
D. Bert and R. Echahed. Design and implementation of a generic, logic and functional programming language. In Proceedings of ESOP'86, number 213 in LNCS, pages 119–132. Springer-Verlag, 1986.
D. Bert et al. Reference manual of the specification language LPG. Technical Report 59, LIFIA, mars 1990. Anonymous ftp at imag.fr, in/pub/SCOP/LPG/NewSun4/man_lpg.dvi.
M. Bidoit. The stratified loose approach: A generalization of initial and loose semantics. Technical Report 402, Université d'Orsay, France, 1988.
C. Choppy. About the “correctness” and “adequacy” of PLUSS specifications. In Recent Trends in Data Type Specifications, number 785 in LNCS, pages 128–143. Springer-Verlag, 1992.
H. Ehrig and B. Mahr. Fundamentals of algebraic specification 1. Equations and initial semantics, volume 6 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1985.
H. Ehrig and B. Mahr. Fundamentals of algebraic specification 2. Module Specifications and Constraints, volume 21 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1990.
K. Futatsugi, J.A. Goguen, J.-P. Jouannaud, and J. Meseguer. Principles of OBJ2. In Proc. Principles of Programming Languages, pages 52–66, 1985.
M.-C. Gaudel. A first introduction to PLUSS. Technical report, Université d'Orsay, France, 1984.
J.A. Goguen, C. Kirchner, H. Kirchner, A. Mégrelis, J. Meseguer, and T. Winkler. An introduction to OBJ3. In Proceedings of the 1 st International Workshop on Conditional Term Rewriting Systems, number 308 in LNCS. pages 258–263. Springer-Verlag, 1987.
S. B. Lippman. C++ Primer. Addison-Wesley, 1992.
F. Nourani. On induction for programming logic. EATCS Bulletin, 13:51–63, 1981.
J.C. Reynaud. Sémantique de LPG. Research Report 651 I IMAG, LIFIA, mars 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bert, D., Oriat, C. (1995). A model inference system for generic specification with application to code sharing. In: Mosses, P.D., Nielsen, M., Schwartzbach, M.I. (eds) TAPSOFT '95: Theory and Practice of Software Development. CAAP 1995. Lecture Notes in Computer Science, vol 915. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-59293-8_232
Download citation
DOI: https://doi.org/10.1007/3-540-59293-8_232
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-59293-8
Online ISBN: 978-3-540-49233-7
eBook Packages: Springer Book Archive