Context transformers in K Framework

A large part of today’s programming languages research and development effort is motivated by the new requirements arising from hardware evolution and software development. Programming languages are becoming more and more complex, requiring precise specifications and tools for defining, testing and analyzing them. One of the most effective ways to define a programming language or paradigm is as an executable formal specification which can both execute programs and formally reason about them. A framework aiming at this goal is K. K is a rewriting-based semantic definitional framework which started in 2003 as a means to define executable concurrent languages in Maude. 
A K definition for a programming language is compiled into a rewrite theory by applying some transformations steps. One of them is the contextual transformation. To improve the modularity of definitions, a K rule only specifies the minimal required context for its application. The contextual transformation step uses static information about the structure of the global running configuration to infer sufficiently additional context to make the rule match and apply on the running configuration.
Although the K-Maude prototype already provides an implementation for context trans- formations, this implementations lacks certain features which are important for the develop- ment of complex definitions, such as the K definition for the C language. Some limitations of the existing approach are that (1) the configuration cannot contain cells with the same name, (2) the cases where the context transformations could have more than one solution are not analyzed, and (3) the locality principle does not have yet an unanimously agreed formal specification. An investigation of all these limitations is required in order to find correct formal definitions which can then be combined to obtain a well-defined contextual transformation algorithm.