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 <>
Submitted on : Friday, September 21, 2007 - 12:01:53 PM
Last modification on : Friday, February 26, 2021 - 3:28:05 PM


  • 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