HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Book sections

Validating and Animating Higher-Order Recursive Functions in B

Michael Leuschel Dominique Cansell 1 Michael Butler
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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.
Document type :
Book sections
Complete list of metadata

Contributor : Dominique Cansell Connect in order to contact the contributor
Submitted on : Friday, September 21, 2007 - 12:01:53 PM
Last modification on : Friday, February 4, 2022 - 3:30:12 AM


  • HAL Id : inria-00174013, version 1



Michael Leuschel, Dominique Cansell, Michael Butler. Validating and Animating Higher-Order Recursive Functions in B. Jean-Raymond Abrial and Uwe Glässer. Festschrift for Egon Börger, Springer-Verlag, 2007, LNCS. ⟨inria-00174013⟩



Record views