Abstract
The B Method is a formal method mainly used in the railway industry to specify and develop safety-critical software. To guarantee the consistency of a B project, one decisive challenge is to show correct a large amount of proof obligations, which are mathematical formulæ expressed in a classical set theory extended with a specific type system. To improve automated theorem proving in the B Method, we propose to use a first-order sequent calculus extended with a polymorphic type system, which is in particular the output proof-format of the tableau-based automated theorem prover Zenon. After stating some modifications of the B syntax and defining a sound elimination of comprehension sets, we propose a translation of B formulæ into a polymorphic first-order logic format. Then, we introduce the typed sequent calculus used by Zenon, and show that Zenon proofs can be translated to proofs of the initial B formulæ in the B proof system.
This work is supported by the BWare project (ANR-12-INSE-0010) funded by the INS programme of the French National Research Agency (ANR).
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
References
Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)
Blanchette, J.C., Böhme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 493–507. Springer, Heidelberg (2013). doi:10.1007/978-3-642-36742-7_34
Bobot, F., Filliâtre, J.C., Marché, C., Paskevich, A.: Why3: shepherd your herd of provers. In: International Workshop on Intermediate Verification Languages (Boogie) (2011)
Bodeveix, J.-P., Filali, M.: Type synthesis in B and the translation of B to PVS. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002. LNCS, vol. 2272, pp. 350–369. Springer, Heidelberg (2002). doi:10.1007/3-540-45648-1_18
Boespflug, M., Carbonneaux, Q., Hermant, O.: The \(\lambda \varPi \)-calculus modulo as a universal proof language. In: Proof Exchange for Theorem Proving (PxTP) (2012)
Bonichon, R., Delahaye, D., Doligez, D.: Zenon: an extensible automated theorem prover producing checkable proofs. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 151–165. Springer, Heidelberg (2007). doi:10.1007/978-3-540-75560-9_13
Bury, G., Delahaye, D., Doligez, D., Halmagrand, P., Hermant, O.: Automated deduction in the B set theory using typed proof search and deduction modulo. In: LPAR 20 : 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Suva, Fiji (2015)
Cauderlier, R., Halmagrand, P.: Checking Zenon modulo proofs in Dedukti. In: Fourth Workshop on Proof eXchange for Theorem Proving (PxTP), Berlin, Germany (2015)
Delahaye, D., Doligez, D., Gilbert, F., Halmagrand, P., Hermant, O.: Zenon modulo: when achilles outruns the tortoise using deduction modulo. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 274–290. Springer, Heidelberg (2013). doi:10.1007/978-3-642-45221-5_20
Delahaye, D., Dubois, C., Marché, C., Mentré, D.: The Bware project: building a proof platform for the automated verification of B proof obligations. In: Ameur, Y.A., Schewe, K.-S. (eds.) Abstract State Machines, Alloy, B, VDM, and Z (ABZ). LNCS, vol. 8477, pp. 290–293. Springer, Heidelberg (2014)
Dowek, G., Hardin, T., Kirchner, C.: Theorem proving Modulo. J. Autom. Reasoning (JAR) 31, 33–72 (2003)
Dowek, G., Miquel, A.: Cut elimination for zermelo set theory. Archive for Mathematical Logic. Springer, Heidelberg (2007, submitted)
Jacquel, M., Berkani, K., Delahaye, D., Dubois, C.: Verifying B proof rules using deep embedding and automated theorem proving. Softw. Eng. Formal Methods 7041, 253–268 (2011)
Jaeger, É., Dubois, C.: Why would you trust B? In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 288–302. Springer, Heidelberg (2007). doi:10.1007/978-3-540-75560-9_22
Kleene, S.C.: Permutability of inferences in Gentzens calculi LK and LJ. In: Bulletin Of The American Mathematical Society, vol. 57, pp. 485–485. Amer Mathematical Soc, Providence (1951)
Mentré, D., Marché, C., Filliâtre, J.-C., Asuka, M.: Discharging proof obligations from Atelier B using multiple automated provers. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 238–251. Springer, Heidelberg (2012). doi:10.1007/978-3-642-30885-7_17
Schmalz, M.: Formalizing the logic of event-B. Ph.D. thesis, Diss., Eidgenössische Technische Hochschule ETH Zürich, Nr. 20516, 2012 (2012)
ClearSy: Atelier B 4.1 (2013). http://www.atelierb.eu/
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Halmagrand, P. (2016). Soundly Proving B Method Formulæ Using Typed Sequent Calculus. In: Sampaio, A., Wang, F. (eds) Theoretical Aspects of Computing – ICTAC 2016. ICTAC 2016. Lecture Notes in Computer Science(), vol 9965. Springer, Cham. https://doi.org/10.1007/978-3-319-46750-4_12
Download citation
DOI: https://doi.org/10.1007/978-3-319-46750-4_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-46749-8
Online ISBN: 978-3-319-46750-4
eBook Packages: Computer ScienceComputer Science (R0)