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.
Type de document :
Chapitre d'ouvrage
Jean-Raymond Abrial and Uwe Glässer. Festschrift for Egon Börger, Springer-Verlag, 2007, LNCS
Liste complète des métadonnées

https://hal.inria.fr/inria-00174013
Contributeur : Dominique Cansell <>
Soumis le : vendredi 21 septembre 2007 - 12:01:53
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52

Identifiants

  • HAL Id : inria-00174013, version 1

Collections

Citation

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〉

Partager

Métriques

Consultations de la notice

134