K Overview and SIMPLE Case Study

Grigore Rosu and Traian Florin Serbanuta
K'11 Elsevier, Volume 304, pp 3-56, June 2014

Abstract. 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.