Dorel Lucanu, Traian Florin Serbanuta
CinK is a kernel of the C++ language we used to experiment with K. The language is used an example for teachingclasses and is refered in several research papers.
In this report we briefly present the K definition of CinK. The most part of the text is automatically generatedwith the K tool, therefore there are some differences between the source code and the pdf version. For instance,the terminal syntax declarations are enclosed into quotes but in the pdf version these are not displayed. In thepdf version, for ease of reading reasons, there are used different fonts in order to distinguish between differentsyntactic categories.
The report is not intended to be an introduction to K. We assume the reader is already familiar with theK Framework and the K tool and here we try to share our experience in defining a languages with some specificfeatures, as C++ is. Such features includes a clear distinction between l-values and r-values, declaration of aliases,and various parameters passing mechanisms. We also extend the definition with a small property language,including LTL formulas, and we show how the K tool is used together with Maude system for analazing CinKprograms.
The K definition of CinK is continuously evolving, so this report presents the status of this definition at thepublication date.
Bibtex
@TechReport{CinKtr,
author = "Dorel Lucanu and Traian Florin Serbanuta",
title = "{CinK – an exercise on how to think in {$mathbf{K}$}}",
institution = "``Al.I.Cuza'' University of Ia{c s}i, Faculty of Computer Science",
year = "2012",
number = "TR 12-03",
url = "https://publications.info.uaic.ro/technical-reports/archive/tr12-03-2012-cink-an-exercise-on-how-to-think-in-k/"
}