K: Overview and SIMPLE Case Study

This paper gives an overview of the tool-supported K framework for semantics-based programming language design and formal analysis.  K provides a convenient notation for modularly defining the syntax and the semantics of a programming language, together with a series of tools based on these, including a parser and an interpreter.  A case study is also discussed, namely the K definition of the dynamic and static semantics of SIMPLE, a non-trivial imperative programming language. 

The material discussed in this paper was presented in an invited talk at the K’11 workshop.