Abstract
ProB is an animation and model checking tool for the B Method, which can deal with many interesting specifications. Some specifications, however, contain complicated functions which cannot be represented explicitly by a tool. We present a scheme with which higher-order recursive functions can be encoded in B, and establish soundness of this scheme. We then describe a symbolic representation for such functions. This representation enables ProB to successfully animate and model check a new class of relevant specifications, where animation is especially important due to the involved nature of the specification.
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.
References
Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)
Abrial, J.-R., Cansell, D., Laffitte, G.: Higher-order mathematics in B. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 370–393. Springer, Heidelberg (2002)
Abrial, J.-R., Mussat, L.: On using conditional definitions in formal theories. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 242–269. Springer, Heidelberg (2002)
Butler, M.: A system-based approach to the formal development of embedded controllers for a railway. Design Automation for Embedded Systems 6(4), 355–366 (2002)
Cansell, D., Méry, D.: Foundations of the B method. Computing and informatics 22(3–4), 221–256 (2003)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice-Hall, Englewood Cliffs (1993)
Krauss, A.: Partial recursive functions in higher-order logic. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 589–603. Springer, Heidelberg (2006)
Leuschel, M., Butler, M.: ProB: A model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003)
Leuschel, M., Butler, M.: Automatic refinement checking for B. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, pp. 345–359. Springer, Heidelberg (2005)
Massart, T., Devillers, R.: Equality of agent expressions is preserved under an extension of the universe of actions. Formal Aspects of Computing 5(1), 79–88 (1993)
Plagge, D., Leuschel, M.: Validating Z Specifications using the ProB Animator and Model Checker. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 480–500. Springer, Heidelberg (2007)
Robertson, J.S.: How many recursive calls does a recursive function make? SIGCSE Bull. 31(2), 60–61 (1999)
Robinson, K.: Reconciling axiomatic and model-based specifications using the B method. In: Bowen, J.P., Dunne, S., Galloway, A., King, S. (eds.) B 2000, ZUM 2000, and ZB 2000. LNCS, vol. 1878, pp. 95–106. Springer, Heidelberg (2000)
Roy, P.V., Haridi, S.: Concepts, Techniques, and Models of Computer Programming. MIT Press, Cambridge (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Leuschel, M., Cansell, D., Butler, M. (2009). Validating and Animating Higher-Order Recursive Functions in B. In: Abrial, JR., Glässer, U. (eds) Rigorous Methods for Software Construction and Analysis. Lecture Notes in Computer Science, vol 5115. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11447-2_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-11447-2_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11446-5
Online ISBN: 978-3-642-11447-2
eBook Packages: Computer ScienceComputer Science (R0)