[GFL04] Synthesizing B Substitutions for EB3 Attribute Definitions

Rapport Scientifique : Date de dépot: 2004/01/01, (Tech. Rep.: CEDRIC-04-683)
Résumé: In this technical report, we show how to synthesize B substitutions from EB3 attribute definitions. The substitutions are obtained by an analysis of CAML-like patterns used in the recursive functions that define the attributes in EB3. We present two ways to generate B substitutions. Either we generate substitution formulas, that take all the B substitutions for each attribute definition into account, and then usual B substitutions are derived from them; or B substitutions are directly synthesized from EB3 attribute definitions by analysing binary trees. The two techniques are illustrated by an example of a library management system.


@techreport {
title="{Synthesizing B Substitutions for EB3 Attribute Definitions}",
author="F. Gervais and M. Frappier and R. Laleau",
institution="{CEDRIC laboratory, CNAM-Paris, France}",