Validating and Animating Higher-Order Recursive Functions in B

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.

• Type: Conference
• Year: 2009
• Where: BIRTHDAY
• Authors: Michael Leuschel, Dominique Cansell, Michael J. Butler
• Keywords: Applied Computing, BIRTHDAY 2009, Model Checking Tool, ProB, Representation Enables Prob