Abstract
We develop within higher order logic (HOL) a general and flexible method of abstraction and refinement, which specifically addresses the problem of handling constraints. We provide a HOL interpretation of first-order Lax Logic, which can be seen as a modal extension of deliverables. This provides a new technique for automating reasoning about behavioural constraints by allowing constraints to be associated with, but formally separated from, an abstracted model. We demonstrate a number of uses, e.g. achieving a formal separation of the logical and timing aspects of hardware design, and systematically generating timing constraints for a simple sequential device from a formal proof of its abstract behaviour. The method and proofs have been implemented in Isabelle as a definitional extension of the HOL logic which extends work by Jacobs and Melham on encoding dependent types in HOL. We assume familiarity with HOL but not detailed knowledge of circuit design.
This work was partially supported by EPSRC under grant GR/L86180.
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
H. Eveking. Behavioural consistency between register-transfer-and switch-level descriptions. In D. A. Edwards, editor, Design Methodologies for VLSI and Computer Architecture. Elsevier Science, B. V., 1989.
M. Fairtlough, M. Mendler, and M. Walton. First-order Lax Logic as a Framework for CLP. Technical Report MIPS-9714, Passau University, Department of Mathematics and Computer Science, 1997.
M. Fairtlough and M. V. Mendler. Propositional Lax Logic. Information and Computation, 137(1):1–33, August 1997.
M. Fairtlough and M. Walton. Quantified Lax Logic. Technical Report CS-97-11, Sheffield University, Department of Computer Science, 1997.
M.P. Fourman. Proof and design. Technical Report ECS-LFCS-95-319, Edinburgh University, Department of Computer Science, 1995.
M.P. Fourman and R.A. Hexsel. Formal synthesis. In G. Birtwistle, editor, Proceedings of the IV Higher Order Workshop, Banff, 1990, 1991.
F. Giunchiglia and T. Walsh. A theory of abstraction. Artificial Intelligence, 57:323–389, 1992.
F.K. Hanna and N. Daeche. Specification and verification using higher order logic: A case study. In G. M. Milne and P. A. Subrahmanyam, editors, Formal Aspects of VLSI design, Proc. of the 1985 Edinburgh conf. on VLSI, pages 179–213. North-Holland, 1986.
J. Herbert. Formal reasoning about timing and function of basic memory devices. In Dr. Luc Claesen, editor, IMEC-IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, Volume 2, pages 668–687. Elsevier Science Publishers, B.V., 1989.
B. Jacobs and T. Melham. Translating dependent type theory into higher order logic. In Typed Lambda Calculi and Applications, TLCA’93, pages 209–229. Springer LNCS 664, 1993.
J.H. McKinna. Deliverables: A Categorical Approach to Program Development in Type Theory. PhD thesis, Edinburgh University, Department of Computer Science, 1992.
T.F. Melham. Higher Order Logic and Hardware Verification. Cambridge University Press, 1993.
M. Mendler. A Modal Logic for Handling Behavioural Constraints in Formal Hardware Verification. PhD thesis, Edinburgh University, Department of Computer Science, ECS-LFCS-93-255, 1993.
M. Mendler. Timing refinement of intuitionistic proofs and its application to the timing analysis of combinational circuits. In P. Miglioli, U. Moscato, D. Mundici, and M. Ornaghi, editors, Proc. 5th Int. Workshop on Theorem Proving with Analytic Tableaux and Related Methods, pages 261–277. Springer, 1996.
M. Mendler and M. Fairtlough. Ternary simulation: A refinement of binary functions or an abstraction of real-time behaviour? In M. Sheeran and S. Singh, editors, Proc. 3rd Workshop on Designing Correct Circuits (DCC’96). Springer Electronic Workshops in Computing, 1996.
D.A. Plaisted. Theorem proving with abstraction. Artificial Intelligence, 16:47–108, 1981.
A.S. Troelstra. Realizability. In S. Buss, editor, Handbook of Proof Theory. Elsevier Science B.V., 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fairtlough, M., Mendler, M., Cheng, X. (2001). Abstraction and Refinement in Higher Order Logic. In: Boulton, R.J., Jackson, P.B. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2001. Lecture Notes in Computer Science, vol 2152. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44755-5_15
Download citation
DOI: https://doi.org/10.1007/3-540-44755-5_15
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42525-0
Online ISBN: 978-3-540-44755-9
eBook Packages: Springer Book Archive