Applying the B formal method to the Bossa domain-specific language

National audienceIntroduction : Domain-specific languages (DSLs) are used in both industry and research, in complex areas as varied as data mining [5], graphics [7], and device driver development [10]. A DSL provides high-level domain-specific abstractions that encapsulate domain expertise, thus making programming easier and less error-prone. Such languages also promise to be more amenable to verification, as the set of language abstractions can be designed to be easy to relate to desired properties and can be constrained to avoid problematic constructs such as unbounded loops. Nevertheless, many DSLs provide no verification, and those that do typically either rely on verification provided by a general-purpose host language or use ad hoc analyzers. The former approach is, however, limited to the facilities of the host language, which are rarely adequate for expressing and checking domain-specific properties, while the latter puts a huge burden on the DSL developer. We observe that many powerful verification systems have been developed in the formal methods community. Our goal is to realize the potential for verification of DSLs by harnessing these resources in designing and implementing DSL verifiers