Abstract
The notion of abstract data types appears in recent languages (CLU, ALPHARD, EUCLID, ADA), for reasons of modularity and protection. Although an algebraïc specification of abstract data types has been developped (Guttag, ADJ), the connection between program semantics and data type semantics has not yet been established, like it was made for the axiomatization of PASCAL. In this paper, we show that the language semantics is composed by a fixed part : the control structure semantics and by an extensible part : the data type semantics. As a consequence, we can, for example, deduce the axiom of the assignement to a subscripted variable from the axioms of the array data type. Finally, we study how to prove that a representation module of an abstract data type is correct w.r.t. its algebraic specification i.e., that it satisfies the algebraic equations.
Chapter PDF
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.
5 — Bibliographie
Preliminary ADA Reference Manual SIGPLAN Notices, vol.14, 6, part A, June 1979
J.W. de BAKKER Correctness proofs for assignment statements Report IW 55/76, Mathematical Center, Amsterdam, 1976
J.W. de BAKKER Semantics and the foundations of program proving Information processing 77, B. Gilchrist, ed., IFIP, 1977, Toronto
BERT D., JACQUET P. Generic abstract data types Proc. 5th Annual III Conference, WG 2.1., IFIP, mai 1977
BERT D. La programmation générique: construction de logiciel, spécification algébrique et vérification Thèse d'Etat, Université de Grenoble I, Labo.IMAG, 1979
R.M. BURSTALL, J.A. GOGUEN Putting theories together to make specifications Proc. Fifth Int. Joint Conf. on artificial intelligence, 1977 MIT, Cambridge, Mass. pp. 1045/1058
J.E. DONAHUE Locations considered unnecessary Acta Informatica 8, pp. 221/242, 1977
J.P.FINANCE De la spécification abstraite d'une donnée à sa représentation en mémoire: les états successifs d'une information Théorie et techniques de l'informatique, Actes du congrès AFCET, novembre 78, pp. 423/433.
J.A.GOGUEN, J.W.THATCHER, E.G.WAGNER An initial algebra approach to the specification,correctness and implementation of abstract data types IBM Research report, RC 6487, octobre 1976.
J.A.GOGUEN Abstract errors for abstract data types Proc. IFIP Working conference on formal description of programming concepts MIT, 1977
J.V.GUTTAG, E.HOROWITZ, D.R.MUSSER Abstract data types and software validation University of Southern California, report ISI/RR 76 48, août 1976
J.V. GUTTAG, J.J. HORNING The Algebraic specification of abstract data types Acta Informatica, 10, pp. 27/52, 1978
J.V.GUTTAG, J.STAUNSTRUP Algebraic axioms, classes and program verification Computer science department, University of Southern California Rapport no 213 741 6288, mars 1978
C.A.R. HOARE Proof of correctness of data representations Acta Informatica, 1, 4, 1972, pp. 271/281
C.A.R. HOARE, N. WIRTH An axiomatic definition of the programming language PASCAL Acta Informatica, 2, pp. 335/355, 1973
B.W.LAMPSON, J.J.HORNING, R.L.LONDON, J.G.MITCHELL, G.L.POPEK Report on the programming language EUCLID SIGPLAN Notices, vol. 12, no2, 1977
B. LISKOV, S. ZILLES Programming with abstract data types Proc. of the ACM SIGPLAN Conference on very high level languages SIGPLAN Notices, 9, 4, 1974, pp. 50/59
B. LISKOV, A. SNYDER, R. ATKINSON, C. SCHAFFERT Abstraction mechanisms in CLU CACM, vol.20, no8, pp. 564/576, 1977
R.E. MILNE, C. STRACHEY A theory of programming language semantics Chapman and Hall, London, Wiley New-York, 1977
R.NAKAJIMA, M.HONDA, H.NAKAHARA Describing and verifying programs with abstract data types Proc. of IFIP Working conference on the formal description of programming concepts, MIT (1977)
J.E.STOY Denotational semantics: The Scott-Strachey approach to programming language theory MIT Press, 1977
R.D. TENNENT The Denotational Semantics of programming languages CACM, 19, 8, august 1976
R.D. TENNENT On a new approach to representation independent data classes Acta Informatica, vol.8, fasc.4, 1977, pp. 315/324
J.W.THATCHER, E.G.WAGNER, J.B.WRIGTH Data type specification: parameterization and the power of specification techniques Proc. 10th SIGACT Symposium on theory of computing, San Diego, CA, 1978
W.A.WULF, R.L.LONDON, M.SHAW Abstraction and verification in ALPHARD: introduction to language and methodology ISI/RR, 74–76, University of California, 1976
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1980 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bert, D. (1980). Types algebriques et semantique des langages de programmation. In: Robinet, B. (eds) International Symposium on Programming. Programming 1980. Lecture Notes in Computer Science, vol 83. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-09981-6_3
Download citation
DOI: https://doi.org/10.1007/3-540-09981-6_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-09981-9
Online ISBN: 978-3-540-39233-0
eBook Packages: Springer Book Archive