Executable Component-Based Semantics

By L. Thomas van Binsbergen, Peter D. Mosses and Neil Sculthorpe

Abstract

The potential benefits of formal semantics are well known. However, it requires a lot of work to produce a complete and accurate formal semantics for a major language; and when the language evolves, large-scale revision of the semantics may be needed to reflect the changes. The investment of effort needed to produce an initial definition, and subsequently to revise it, has discouraged language developers from using formal semantics. Consequently, many major programming languages (and most domain-specific languages) do not yet have formal semantic definitions.

To improve the practicality of formal semantic definitions, the PLanCompS project has developed a component-based approach. In this approach, the semantics of a language is defined by translating its constructs (compositionally) to combinations of so-called fundamental constructs, or `funcons’. Each funcon is defined using a modular variant of structural operational semantics, and forms a language-independent component that can be reused in definitions of different languages. A substantial library of funcons has been developed and tested in several case studies. Crucially, the definition of each funcon is fixed, and does not need changing when new funcons are added to the library.

For specifying component-based semantics, we have designed and implemented a meta-language called CBS. CBS includes specification of abstract syntax, of its translation to funcons, and of the funcons themselves. Development of CBS specifications is supported by an integrated development environment. The accuracy of a language definition can be tested by executing the specified translation on programs written in the defined language, and then executing the resulting funcon terms. This paper gives an introduction to CBS, illustrates its use, and presents the various tools involved in our implementation of CBS.

Accompanying material

The archive below accompanies an article submitted to the Journal of Logical and Algebraic Methods in Programming.

CBS-SIMPLE.tar.gz (updated 11/03/2016)

The archive includes:

  • A CBS library of funcon definitions;
  • A Spoofax editor for CBS files;
  • A Haskell-based compiler from CBS funcon definitions to Haskell-embedded funcons;
  • A CBS definition of the SIMPLE language;
  • A Spoofax editor for SIMPLE programs;
  • An extension for the Haskell-based funcon interpreter that includes the SIMPLE-specific funcons;
  • A collection of SIMPLE test programs, and the corresponding funcon terms.

A Haskell-based interpreter for funcon terms is available on Hackage.