Abstract
Formal methods tools vary widely but generally have logical foundations. For ACL2, a general purpose theorem prover under continuous development since about 1990, having a sound logical foundation is absolutely essential. Many formal tools support execution on concrete data, and ACL2 does so by being compatible with the Common Lisp language: theorems can be proved about Common Lisp functions in the ACL2 subset, and efficient execution is provided by reliance on compiled Common Lisp code. ACL2’s arithmetic is based on a straightforward axiomatization of the rationals and Common Lisp provides exact rational arithmetic. But computation based on exact rational arithmetic is relatively slow, so we have recently added support for floating-point operations in ACL2. The challenge is how to do this while preserving the pre-existing axioms for arithmetic and a large regression suite containing verified theorems and other logical tools contributed and used by the entire ACL2 community. We discuss how we have met these challenges, we discuss the limitations of our support for floating-point operations, and we illustrate the resulting system with examples.
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
Similar content being viewed by others
Notes
- 1.
Recall we are ignoring ACL2’s handling of complex rationals here. And the standard does not say that (+ x y) is the sum — in the ordinary mathematical sense of that word — for floating-point numbers because it is not!.
- 2.
Actually, the story is more complicated than this. But this basic idea that every definition in the logic gives rise to two definitions in the underlying Lisp is suggestive of what really happens.
- 3.
This is not the first use of typed syntax in ACL2. See [2].
- 4.
The astute reader may observe that the inputs are the rationals 3/2 and 1/4, yet previous discussion may have suggested that the arguments to df+ should be df expressions. In fact df+ is a macro and rational arguments are converted to dfs, as discussed below in Subsect. 6.3.
- 5.
In ACL2 and Common Lisp, symbol names are case insensitive by default.
References
ACL2 User Community: ACL2 community books. https://github.com/acl2/acl2/tree/master/books
Boyer, R.S., Moore, J.S.: Single-threaded objects in ACL2. In: Krishnamurthi, S., Ramakrishnan, C.R. (eds.) Practical Aspects of Declarative Languages, 4th International Symposium, PADL 2002, Portland, OR, USA, January 19-20, 2002, Proceedings. Lecture Notes in Computer Science, vol. 2257, pp. 9–27. Springer (2002). https://doi.org/10.1007/3-540-45587-6_3, https://doi.org/10.1007/3-540-45587-6_3
Brock, B., Kaufmann, M., Moore, J.S.: ACL2 theorems about commercial microprocessors. In: Srivas, M., Camilleri, A. (eds.) Formal Methods in Computer-Aided Design (FMCAD’96), pp. 275–293. Springer-Verlag, LNCS 1166, Heidelberg (November 1996). https://doi.org/10.1007/BFb0031816, http://www.cs.utexas.edu/users/moore/publications/bkm96.ps.Z
Hunt, Jr., W., Kaufmann, M., Moore, J.S., Slobodova, A.: Industrial hardware and software verification with ACL2. In: Verified Trustworthy Software Systems. vol. 375. The Royal Society (2017).https://doi.org/10.1098/rsta.2015.0399, (Article Number 20150399)
Hunt, Jr., W.A., Ramanathan, V., Moore, J.S.: Vwsim: A circuit simulator. In: Sumners, R., Chau, C. (eds.) Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022. Electronic Proceedings in Theoretical Computer Science, vol. 359, pp. 61–75. Open Publishing Association (2022). https://doi.org/10.4204/EPTCS.359.7
Kaufmann, M., Manolios, P., J S. Moore: Computer-Aided Reasoning: An Approach. Kluwer Academic Press, Boston, MA. (2000). https://doi.org/10.1007/978-1-4615-4449-4
Kaufmann, M., Moore, J.S.: The ACL2 home page. In: Department of Computer Sciences, University of Texas at Austin (2024). http://www.cs.utexas.edu/users/moore/acl2/
Kaufmann, M., J S. Moore: ACL2 Documentation for DF. http://acl2.org/manual/index.html?topic=ACL2____DF
Kaufmann, M., J S. Moore: ACL2 Documentation for Partial Encapsulation. http://acl2.org/manual/index.html?topic=ACL2____PARTIAL-ENCAPSULATE
Kaufmann, M., J S. Moore: ACL2 Documentation for TERM. http://acl2.org/manual/index.html?topic=ACL2____TERM
Kaufmann, M., J S. Moore, The ACL2 Community: The Combined ACL2+Books User’s Manual. http://acl2.org/manual/index.html (2021)
LispWorks: Common Lisp Documentation. http://www.lispworks.com/documentation/common-lisp.html
Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D., et al. (eds.) Automated Deduction—CADE-11, pp. 748–752. Springer Berlin Heidelberg, Berlin, Heidelberg (1992). https://doi.org/10.1007/3-540-55602-8_217
Pitman, K.: The Common Lisp HyperSpec. https://www.lispworks.com/documentation/HyperSpec/Front/
Russinoff, David M.: Formal Verification of Floating-Point Hardware Design: A Mathematical Approach, 2nd edn. Springer International Publishing, Cham (2022). https://doi.org/10.1007/978-3-030-87181-9
Standards Committee of the IEEE Computer Society: IEEE standard for binary floating-point arithmetic. Tech. Rep. IEEE Std. 754-1985, IEEE, 345 East 47th Street, New York, NY 10017 (1985)
Acknowledgments
We thank ForrestHunt, Inc. for support for this work. We especially thank Warren Hunt for encouraging us to pursue support for floating point in ACL2. For a long time we did not see a way to do it without changing the logic (e.g., the axioms for equality and arithmetic). That in turn would have required changes to the regression suite too numerous to mention. But Warren was insistent that we keep trying and we ultimately discovered the method described here. Thank you Warren, not just for the support but for the encouragement. We also thank the reviewers for excellent feedback, which has resulted in a number of improvements.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Ethics declarations
Disclosure of Interests
The authors have no competing interests to declare that are relevant to the content of this article.
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this chapter
Cite this chapter
Kaufmann, M., Moore, J.S. (2024). ACL2 Support for Floating-Point Computations. In: Cavalcanti, A., Baxter, J. (eds) The Practice of Formal Methods. Lecture Notes in Computer Science, vol 14780. Springer, Cham. https://doi.org/10.1007/978-3-031-66676-6_13
Download citation
DOI: https://doi.org/10.1007/978-3-031-66676-6_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-66675-9
Online ISBN: 978-3-031-66676-6
eBook Packages: Computer ScienceComputer Science (R0)