Abstract
This paper illustrates how animation conversions [14] which help in preliminary debugging of behavioural definitions, can subsequently be used as effective proof tools which play an important role in the verification of properties related to the definitions. We illustrate this point by specifying a simple compiler to map constructs of a toy imperative programming language into instructions which run on a rudimentary abstract machine. The same conversions used to symbolically compile programs of the language and to execute the resulting machine instructions are used in the verification of the compiler. This paper suggests that conversions provide a sound basis for a proof methodology with formal animation acting as an integral step in a verification process.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Aagaard and Leeser: Verifying a logic synthesis tool in Nuprl. 4th Workshop on Computer Aided Verification. (1992)
R. Boulton, M. Gordon, J. Herbert, and J. Van Tassel: The HOL Verification of ELLA Designs. Technical Report 199, University of Cambridge Computer Laboratory, August 1990. Revised version in the Proceedings of the International Workshop on Formal Methods in VLSI Design, Miami. (1991)
Albert John Camilleri: Executing Behavioural Definitions in Higher Order Logic. Ph.D. thesis, University of Cambridge Computer Laboratory. (1988)
Juanito Camilleri: Symbolic Compilation and Execution of Programs by Proof: A case study in HOL. Technical Report 240, University of Cambridge Computer Laboratory. (1991)
Juanito Camilleri and T.F. Melham: Reasoning with Inductively Defined Relations in the HOL Theorem Prover. Technical Report 265, University of Cambridge Computer Laboratory. (1992)
Paul Curzon: A verified compiler for a structured assembly language. In Proc. 4th International HOL Users Meeting. (1991)
Paul Curzon: Of what use is a verified compiler specification? Technical Report 274, University of Cambridge Computer Laboratory. (1992)
M.J.C. Gordon: HOL — A Machine Oriented Formulation of Higher Order Logic. Technical Report 68, University of Cambridge Computer Laboratory. (1985)
Matthew Hennessy: The Semantics of Programming Languages: An Elementary Introduction using Structural Operational Semantics. Wiley. (1990)
Hall and Windley: Simulating microprocessors from formal specifications. Higher Order Logic Theorem Proving and its Applications, Horth Holland. (1992)
J.J. Joyce: A verified compiler for a verified microprocessor. Technical Report 167, Computer Laboratory, University of Cambridge. (1989)
T.F. Melham: Automating Recursive Type Definitions in Higher Order Logic. In Current Trends in Hardware Verification and Automated Deduction, G.Birtwhistle and P.A.Subrahmanyam eds., Springer Verlag. (1988)
T.F. Melham: A package for Inductive Relation Definitions in HOL. In Proc. 4th International HOL Users Meeting. (1991)
Lawrence Paulson: A higher-order implementation of rewriting. In Science of Computer Programming 3 (1983) 119–149
Gordon D. Plotkin: A Structural Approach to Operational Semantics. Technical Report, Department of Computer Science, Aarhus University Denmark. (1981)
Rajan: Executing HOL. In Higher Order Logic Theorem Proving and its Applications. Horth Holland. (1992)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Camilleri, J., Zammit, V. (1994). Symbolic animation as a proof tool. In: Melham, T.F., Camilleri, J. (eds) Higher Order Logic Theorem Proving and Its Applications. HUG 1994. Lecture Notes in Computer Science, vol 859. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58450-1_38
Download citation
DOI: https://doi.org/10.1007/3-540-58450-1_38
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58450-6
Online ISBN: 978-3-540-48803-3
eBook Packages: Springer Book Archive