Parsing K definitions

AbstractThis paper describes our approach in parsing a K definition. The difficulty of the problem is given by the nature of the K-framework, where the user can define the operational semantics of a language by inserting pieces of concrete syntax in the K code in a natural way. Our main contribution shows how to make use of SDF and the disambiguation mechanisms in the context of K-framework