Abstract
Starting from the specification of a small imperative programming language, and the description of two program transformations on this language, we formally prove the correctness of these transformations. The formal specifications are given in a single format, and can be compiled into both executable tools and collections of definitions to reason about into a theorem prover. This work is a case study of an environment integrating executable tool generation and formal reasoning on these tools.
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
I. Attali. Compiling Typol with Attribute Grammars. In Programming Language Implementation and Logic Programming, Orléans, France, 1988. Springer Verlag, LNCS.
G. Berry. Real-time programming: General purpose or special-purpose languages. In G. Ritter, editor, Information Processing 89, pages 11–17. Elsevier Science Publishers P.V, 1989.
Y. Bertot. Une Automatisation du Calcul des Résidus en Sémantique Naturelle. PhD thesis, Université de Nice-Sophia Antipolis, 1991.
Y. Bertot, G. Kahn, and L. Théry. Real Theorem Provers Deserve Real Interfaces. In 5th ACM Symposium on Software Development Environments, Washington, 1992. Also available as INRIA Research Report, RR-1684.
K. Buth. Techniques for Modelling Structured Operational and Denotational Semantics Definitions with Term Rewriting Systems. PhD thesis, Christian-Albrechts University, Kiel, 1994.
J. Camilleri and V. Zammit. Symbolic Animation as a Proof Tool. In HOL Theorem Proving System and its Applications. Springer-Verlag LNCS 859, 1994.
T. Despeyroux. Executable Specifications of Static Semantics. In International Symposium on Semantics of Data Types, 1984. Springer-Verlag LNCS 173.
J. Despeyroux. Proof of Translation in Natural Semantics. In Proceedings of the first ACM-IEEE Symp. on Logic In Computer Science, Cambridge, Ma, USA, June 1986, pages 193–205, 1986. also available as a Research Report RR-514, Inria-Sophia-Antipolis, France, April 1986.
G. Dowek, A. Felty, H. Herbelin, G. Huet, Ch. Paulin, and B. Werner. The Coq Proof Assistant User's guide, Version 5.8. Technical Report 154, INRIA, Rocquencourt, May 1993.
J. Despeyroux and A. Hirschowitz. Higher-Order Abstract Syntax and Induction in Coq. In Proceedings of the 5 th Int. Conf. on Logic Programming and Automated Reasoning, July 1994.
A. Felty and D. Howe. Generalization and Reuse of Tactic Proofs. In Proceedings of the 5 th Int. Conf. on Logic Programming and Automated Reasoning, July 1994.
J.V. Guttag and J.J.Horning, editors. Larch: Languages and Tools for Formal Specification. Springer-Verlag, 1993.
R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Technical Report 162, LFCS, University of Edinburgh, June 1991.
I. Jacobs. The Centaur 1.2 Manual. Technical report, INRIA, Sophia-Antipolis, 1992.
G. Kahn. Natural Semantics. In Proceedings of the Symp. on Theorical Aspects of Computer Science, Passau, Germany, 1987. Also available as Research Report RR-601, INRIA, Sophia-Antipolis, February 1987.
Paul Klint. A Meta-environment for Generating Programming Environments. In ACM Transaction on Software Engineering and Methodology, number 2 in 2, pages 176–201, 1993.
M.J.C. Gordon and T.Melham. HOL: a Proof Generating System for Higher-order Logic. Cambridge University Press, 1992.
F. Pfenning. Elf: A Language for Logic Definition and Verified Meta-Programming. In Proceedings of the 4 th International Symposium on Logic in Computer Science, June 1989.
G.D. Plotkin. A Structural Approach to Operational Semantics. Technical Report DAIMI FN-19, Aarhus, 1981.
C. Paulin-Mohring. Inductive Definitions in the System Coq: Rules and Properties. In Mark Bezem and Jan-Friso Groote, editors, Typed Lambda Calculi and Applications, pages 328–345. Springer-Verlag, March 1993.
F. Pfenning and E. Rohwedder. Implementing the Meta-Theory of Deductive Systems. In D. Kapur, editor, Proceedings of the 11 th International Conference on Automated Deduction, Saratoga Springs, New York, June 1992.
R. Reetz and T. Kropf. Simplifying Deep Embedding: A Formalised Code Generator. In HOL Theorem Proving System and its Applications. Springer-Verlag LNCS 859, 1994.
R. Roxas and M. Newey. Proof of Program Transformations. In HOL'91, HOL Theorem Proving System and its Applications, pages 223–230. IEEE Computer Society Press, 1991.
T. Reps and T. Teitelbaum. The Synthesizer Generator: a System for Constructing Language Based Editors. Springer Verlag, 1988. (third edition).
D. Terrasse. Encoding Natural Semantics in Coq. Submitted to AMAST'95. Also available by anonymous ftp to babar.inria.fr:pub/croap/terrasse:NSinCoq.dvi, 1994.
G. Winskel. The Formal Semantics of Programming Languages, an Introduction. Foundations of Computing. The MIT Press, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bertot, Y., Fraer, R. (1995). Reasoning with executable specifications. 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_218
Download citation
DOI: https://doi.org/10.1007/3-540-59293-8_218
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