Label-Based Programming Language Semantics in K Framework with SDF

A programming language definition consists of two parts: syntax and semantics. K Framework is an actively developed formalism aimed to address the semantics part. While K has its own capabilities to define syntax and to perform parsing, those are often not expressive enough to handle real world programming languages. Therefore K Framework was designed to be connected to an external parser. In this case the semantics is defined over the representation of programs as AST (Abstract Syntax Tree), and is called label-based. This technique was successfully used to define C language. In this paper we present a parser generator which accepts as input a grammar in SDF format, and produces a parser ready to be integrated with K. We illustrate the methodology of defining a language using the generated parser based on an example. The example definition emphasizes distinctive features of the integration of SDF syntax and K semantics. It also illustrates syntax constructs which are difficult to handle with K Framework alone, but are straightforward to express in SDF + K combination.