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.