TY - JOUR
T1 - K overview and SIMPLE case study
AU - Roşu, Grigore
AU - Şerbǎnuţǎ, Traian Florin
N1 - Funding Information:
In spite of its youth, the K framework has already proven to be practical, as it has been used with relatively little effort to define complex languages like Java, Scheme, Verilog, or C, and to use those definitions for analyzing programs written in those languages. K is currently under heavy development, with bugs being fixed and new features and capabilities added on a regular basis. This is all possible due to the enthusiasm and strong belief of its designers and developers that K can be not only an academic exercise but also a solid, practical and scalable tool for programming language design and analysis, as well as due to generous funding under the NSA contract H98230-10-C-0294, the NSF grant CCF-0916893, and the (Romanian) SMIS-CSNR 602-12516 contract no. 161/15.06.2010.
PY - 2014/6/10
Y1 - 2014/6/10
N2 - 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.
AB - 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.
KW - K
KW - Programming Languages
KW - Rewriting-Based Semantics
UR - http://www.scopus.com/inward/record.url?scp=84901773483&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84901773483&partnerID=8YFLogxK
U2 - 10.1016/j.entcs.2014.05.002
DO - 10.1016/j.entcs.2014.05.002
M3 - Article
AN - SCOPUS:84901773483
SN - 1571-0661
VL - 304
SP - 3
EP - 56
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
ER -