Abstract
The use of formal methods provides confidence in the correctness of developments. Yet one may argue about the actual level of confidence obtained when the method itself – or its implementation – is not formally checked. We address this question for the B, a widely used formal method that allows for the derivation of correct programs from specifications. Through a deep embedding of the B logic in Coq, we check the B theory but also implement B tools. Both aspects are illustrated by the description of a proved prover for the B logic.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abrial, J.R.: The B-Book - Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)
The Coq development team: The Coq proof assistant reference manual. LogiCal Project (2004)
Gordon, M.J.C.: Mechanizing programming logics in higher-order logic. In: Birtwistle, G.M., Subrahmanyam, P.A. (eds.) Current Trends in Hardware Verification and Automatic Theorem Proving (Proceedings of the Workshop on Hardware Verification), Banff, Canada, pp. 387–439. Springer, Berlin (1988)
Boulton, R.J., Gordon, A., Gordon, M.J.C., Harrison, J., Herbert, J., Tassel, J.V.: Experience with embedding hardware description languages in hol. In: Stavridou, V., Melham, T.F., Boute, R.T. (eds.) TPCD. IFIP Transactions, North-Holland, vol. A-10, pp. 129–156 (1992)
Azurat, A., Prasetya, I.: A survey on embedding programming logics in a theorem prover. Technical Report UU-CS-2002-007, Institute of Information and Computing Sciences, Utrecht University (2002)
Bodeveix, J.P., Filali, M., Muñoz, C.: A formalization of the B-method in Coq and PVS. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol. 1709, pp. 33–49. Springer, Heidelberg (1999)
Chartier, P.: Formalisation of B in Isabelle/HOL. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, pp. 66–82. Springer, Heidelberg (1998)
Ridge, T., Margetson, J.: A mechanically verified, sound and complete theorem prover for first order logic. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 294–309. Springer, Heidelberg (2005)
Berkani, K., Dubois, C., Faivre, A., Falampin, J.: Validation des règles de base de l’Atelier B. Technique et Science Informatiques 23(7), 855–878 (2004)
Cirstea, H., Kirchner, C.: Using rewriting and strategies for describing the B predicate prover. In: Kirchner, C., Kirchner, H. (eds.) CADE-15. LNCS (LNAI), vol. 1421, pp. 25–36. Springer, Heidelberg (1998)
de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. Indagationes Mathematicae (Proceedings), pp. 381–392 (1972)
Liang, C., Nadathur, G.: Tradeoffs in the intensional representation of lambda terms. In: Tison, S. (ed.) RTA 2002. LNCS, vol. 2378, pp. 192–206. Springer, Heidelberg (2002)
Aydemir, B., Charguéraud, A., Pierce, B.C., Weirich, S.: Engineering aspects of formal metatheory, Manuscript (2007)
Bird, R., Paterson, R.: De Bruijn notation as a nested datatype. Journal of Functional Programming 9, 77–91 (1999)
Abadi, M., Cardelli, L., Curien, P.L., Lévy, J.J.: Explicit substitutions. Journal of Functional Programming 1, 375–416 (1991)
Curien, P.L., Hardin, T., Lévy, J.J.: Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM 43, 362–397 (1996)
Gordon, A.D.: A mechanisation of name-carrying syntax up to alpha-conversion. In: Joyce, J.J., Seger, C.-J.H. (eds.) HUG 1993. LNCS, vol. 780, pp. 413–425. Springer, Heidelberg (1994)
Mussat, L.: Private Communication (2005)
Delahaye, D.: A tactic language for the system Coq. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol. 1955, pp. 85–95. Springer, Heidelberg (2000)
Colin, S., Petit, D., Rocheteau, J., Marcano, R., Mariano, G., Poirriez, V.: BRILLANT: An open source and XML-based platform for rigourous software development. In: SEFM (Software Engineering and Formal Methods), Koblenz, Germany, AGKI (Artificial Intelligence Research Koblenz), IEEE Computer Society Press, Los Alamitos (2005) selectivity : 40/120
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jaeger, É., Dubois, C. (2007). Why Would You Trust B?. In: Dershowitz, N., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2007. Lecture Notes in Computer Science(), vol 4790. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75560-9_22
Download citation
DOI: https://doi.org/10.1007/978-3-540-75560-9_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75558-6
Online ISBN: 978-3-540-75560-9
eBook Packages: Computer ScienceComputer Science (R0)