Resume
Nous présentons un système de preuve de compilateurs, fondé sur le formalisme des types abstraits algébriques et sur le démonstrateur de théoèmes LCF. Un compilateur est spécifié par une fonction de représentation entre deux types abstraits algébriques. Le système produit des conditions de correction de la représentation et un ensemble de théories LCF dans lesquelles sont menées les preuves. Nous fournissons des stratégies pour mener automatiquement la plus grande partie de la preuve, et des tactiques spécialisées pour la terminer interactivement.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
5. Bibliographie
C. BENOIT: "Axiomatisation des tests et systèmes completes de preuve." Thèse de Sème cycle, LITP, Université de Paris-7, 1983.
M.BIDOIT, M.C. GAUDEL: "Etude des méthodes de spécification des cas d'exceptions dans les types abstraits algébriques." CGE, Laboratoires de Marcousis, Décembre 1982.
M.BROY, C.PAIR, M.WIRSING: "A systematic study of models of abstract data types." Nancy, 1981.
M.BROY, M.WIRSING: "Pertial abstract types." Acta informatica No 18, 1982.
Ph.DESCHAMP: "Perluette: a compiler's producing system using abstract data types." 5th Intern. Symp. on Programming, LNCS 137, Turin, Avril 1982.
J.DESPEYROUX: "Une sémantique algébrique de Pascal et application à la spécification d'un compilateur Pascal-P-code." Thèse de 3ème cycle, Université Paris-Sud, Novembre 1982.
H.D.EHRICH: "On the theory of specification, implementation and parametrization of abstract data types." Rapport technique, Forschungsbericht, Dortmund, 1978 et JACM 29, 1982.
H.D. EHRIG, H.J. KREOWSKY: "Parameter passing commutes with implementation of parameterized data types." Proc. 9th ICALP, Aarhus, Danemark, 1982.
H.D.EHRIG, H.J.KREOWSKY, B.MAHR, P.PADAWITZ: "Algebraic implementation for abstract data types." Theorical Computer Science.
M.C.GAUDEL: "Génération et preuve des compilateurs basées sur une sémantique formelle des langages de programmation." Thèse d'état, INPL, Nancy, 1980.
J.V.GUTTAG, J.J.HORNING: "The algebraic specification of abstract data types." Acta informatica 10, No.1, 1978.
J.V.GUTTAG: "Abstract data types and the development of data structures." CACM, Vol.20, No.6, 1977.
E.MADELAINE: "Un système d'aide à la preuve de compilateurs." Thèse de Sème cycle, INRIA-Paris 7, Septembre 1983.
L.PAULSON: "Recent developpement in LCF: examples of structural induction." Rapport No34, Université de Cambridge, Janvier 1983.
L.PAULSON: "Rewriting in Cambridge LCF." Rapport No35, Université de Cambridge, Fèvrier 1983.
D.A.PLAISTED: "An initial algebra semantics for error presentation." Avril 1982.
D. SANELLA, M. WIRSING: "Implementation of parameterized specifications." Proc. 9th ICALP, Aarhus, Danemark, 1982.
M.WIRSING, M.BROY: "Abstract data types as lattices of finitely generated models." 9th MFCS, LNCS 88, Berlin, 1980.
M.WIRSING, M.BROY: "An analysis of semantic models for algebraic specifications". Int. summer school on the theorical foundations of prog. methodology. Marktoberdorf, 1981.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1984 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Madelaine, E. (1984). Un systeme d'aide a la preuve de compilateurs. In: Paul, M., Robinet, B. (eds) International Symposium on Programming. Programming 1984. Lecture Notes in Computer Science, vol 167. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-12925-1_39
Download citation
DOI: https://doi.org/10.1007/3-540-12925-1_39
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-12925-7
Online ISBN: 978-3-540-38809-8
eBook Packages: Springer Book Archive