Abstract
Symbolic functional evaluation (SFE) is the extension of an algorithm for executing functional programs to evaluate expressions in higher-order logic. SFE carries out the logical transformations of expanding definitions, beta-reduction, and simplification of built-in constants in the presence of quantifiers and uninterpreted constants. We illustrate the use of symbolic functional evaluation as a “universal translator” for linking notations embedded in higher-order logic directly with automated analysis without using a theorem prover. SFE includes general criteria for when to stop evaluation of arguments to uninterpreted functions based on the type of analysis to be performed. SFE allows both a novice user and a theorem-proving expert to work on exactly the same specification. SFE could also be implemented in a theorem prover such as HOL as a powerful evaluation tactic for large expressions.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. D. Aagaard, M. E. Leeser, and P. J. Windley. Towards a super duper hardware tactic. In J. J. Joyce and C.-J. H. Seger, editors, HOL User’s Group Workshop. Springer-Verlag, August 1993.
J. H. Andrews. Executing formal specifications by translating to higher order logic programming. In TPHOLs, volume 1275 of LNCS, pages 17–32. Springer Verlag, 1997.
J. H. Andrews, N. A. Day, and J. J. Joyce. Using a formal description technique to model aspects of a global air traffic telecommunications network. In FORTE/PSTV’97, 1997.
J. M. Atlee and J. Gannon. State-based model checking of event-driven system requirements. IEEE Trans. on Soft. Eng., 19(1):24–40, January 1993.
R. Bharadwaj and C. Heitmeyer. Verifying SCR requirements specifications using state space exploration. In Proceedings of the First ACM SIGPLAN Workshop on Automatic Analysis of Software, 1997.
R. Boulton et al. Experience with embedding hardware description languages in HOL. In Theorem Provers in Circuit Design, pages 129–156. North-Holland, 1992.
R. S. Boyer and J. S. Moore. Proving theorems about LISP functions. Jour. of the ACM, 72(1):129–144, January 1975.
R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, August 1986.
J. R. Burch and D. L. Dill. Automatic verification of pipelined microprocessor control. In CAV, volume 818 of LNCS, pages 68–79. Springer-Verlag, 1994.
A. J. Camilleri. Simulation as an aid to verification using the HOL theorem prover. Technical Report 150, University of Cambridge Computer Laboratory, October 1988.
A. Cohn. The notion of proof in hardware verification. Journal of Automated Reasoning, 5(2):127–139, June 1989.
C. Consel and O. Danvy. Tutorial notes on partial evaluation. In POPL, pages 493–501. ACM Press, 1993.
N. Day and J. Joyce. The semantics of statecharts in HOL. In HOL User’s Group Workshop, volume 78, pages 338–351. Springer-Verlag, 1993.
N. A. Day. A Framework for Multi-Notation, Model-Oriented Requirements Analysis. PhD thesis, Department of Computer Science, University of British Columbia, 1998.
N. A. Day, J. J. Joyce, and G. Pelletier. Formalization and analysis of the separation minima for aircraft in the North Atlantic Region. In Fourth NASA Langley Formal Methods Workshop, pages 35–49. NASA Conference Publication 3356, September 1997.
N. A. Day, J. R. Lewis, and B. Cook. Symbolic simulation of microprocessor models using type classes in Haskell. To appear in CHARME’99 poster session.
M. Gordon and T. Melham, editors. Introduction to HOL. Cambridge University Press, 1993.
M. J. C. Gordon. Combining deductive theorem proving with symbolic state enumeration. Transparencies from a presentation, summer 1998.
M. J. C. Gordon. Mechanizing programming logics in higher-order logic. In Current Trends in Hardware Verification and Automated Theorem Proving, pages 387–439. Springer-Verlag, 1988.
D. A. Greve. Symbolic simulation of the JEM1 microprocessor. In FMCAD, volume 1522 of LNCS, pages 321–333. Springer, 1998.
D. Harel. Statecharts: A visual formalism for complex systems. Science of Computing, 8:231–274, 1987.
M. P. Heimdahl and N. G. Leveson. Completeness and consistency in hierarchical state-based requirements. IEEE Trans. on Soft. Eng., 22(6):363–377, June 1996.
C. L. Heitmeyer, R. D. Jeffords, and B. G. Labaw. Automated consistency checking of requirements specifications. ACM Transactions on Software Engineering and Methodology, 5(3):231–261, July 1996.
T. Johnsson. Efficient compilation of lazy evaluation. In Proceedings of the ACM Conference on Compiler Construction, pages 122–32, 1984.
R. B. Jones, D. L. Dill, and J. R. Burch. Efficient validity checking for processor verification. In ICCAD, 1995.
J. Joyce. Multi-Level Verification of Microprocessor Based Systems. PhD thesis, Cambridge Comp. Lab, 1989. Technical Report 195.
J. Joyce, N. Day, and M. Donat. S: A machine readable specification notation based on higher order logic. In International Workshop on the HOL Theorem Proving System and its Applications, pages 285–299, 1994.
N. G. Leveson et al. Requirements specification for process-control systems. IEEE Transactions on Software Engineering, 20(9):684–707, September 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Day, N.A., Joyce, J.J. (1999). Symbolic Functional Evaluation. In: Bertot, Y., Dowek, G., Théry, L., Hirschowitz, A., Paulin, C. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1999. Lecture Notes in Computer Science, vol 1690. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48256-3_23
Download citation
DOI: https://doi.org/10.1007/3-540-48256-3_23
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66463-5
Online ISBN: 978-3-540-48256-7
eBook Packages: Springer Book Archive