Peter D Mosses
Ferdinand Vesely
Department of Computer Science, Swansea University
January 2014
The accompanying files provide a component-based semantics of a series of sublanguages of the CinK language, a kernel of C++ used to experiment with the K Framework, cf. (Lucanu, Serbanuta, and Rosu 2012; Lucanu and Serbanuta 2013)
The main idea of component-based semantics is to translate languages into an open-ended collection of language-independent fundamental constructs, called funcons (Mosses 2008).
Semantics of each funcon is specified (largely) independently, to maximise reusability.
A component-based semantics of the tiny language IMP is provided with the K Tool in k/examples/funcons. The present case study tests the incrementality of the component-based approach, as well as the modularity of the K specifications of the individual funcons and datatypes of values.
A paper with detailed explanations of the approach and the specifications has been submitted to WRLA 2014.
Install a stable release of the K Tool.
chmod u+x .../k/lib/scripts/checkJava
The version of the stable release used for this case study was:
K-framework nightly build.
Git Revision: jenkins-k-framework-git-410
Build date: Fri Oct 11 19:32:41 EEST 2013
Then compile the language specification using the K Tool:
cd .../CinF/languages/L
kompile cinf
This can take a couple of minutes, and should produce no warnings or errors.
cd .../CinF/languages/L
krun tests/P.cinf
Depending on P, you may be asked to input one or more integers.
The result should be the output (if any) followed by the final K configuration.
We provide a script, run-all.sh
, which can be used to run all test programs included in a language folder or in all language folders. Instructions are given at the top of the script.
Each language specification consists of the following files:
cinf-syntax.k
: the language syntaxcinf.k
: rules translating the language syntax to funcons and valuescinf-<language>-funcons.k
: importing the required funconscinf-<language>-values.k
: importing the required valuesThe languages consist of a simple initial language and a series of increments. However, each language is specified monolithically: an increment was produced by copying the syntax and semantics, then editing-in the new language constructs.
As the order in which the language constructs are specified is preserved, the difference between the syntax or semantics of any pair of languages can easily be seen using standard file comparison utilities (e.g., Compare with each other
in Eclipse).
A set of pre-rendered comparisons can be found here.
This pure expression sub-language includes only integer and boolean literals, unary and binary operators, and conditional conjunction and disjunction.
This sub-language adds variable declarations, and extends expressions with identifiers, assignments and the comma operator.
Apart from introducing the usual control flow statements, and block structure, this sub-language extends expressions with input and output.
Compare to previous sub-language: semantics | syntax
Here, top-level declarations are extended to allow function definitions with value parameters. Function bodies are statements, where return statements terminate execution abruptly.
Compare to previous sub-language: semantics | syntax
This extension provides only very basic language support for spawning threads.
Compare to previous sub-language: semantics | syntax
Variable declarations are extended to support references (binding identifiers to existing variables). Function declarations now allow reference parameters and returning references as results.
Compare to previous sub-language: semantics | syntax
Variable declarations and expressions are extended to support pointers.
Compare to previous sub-language: semantics | syntax
The K specifications of all the funcons, each in a separate file:
The K specifications of all the data types of values, each in a separate file:
This case study was inspired by (Lucanu and Serbanuta 2013) and by the translation of IMP to funcons provided in k/examples/funcons.
The K specifications of the funcons correspond to simplified versions of specifications in (Churchill, Mosses, and Torrini 2014).
Churchill, Martin, Peter D. Mosses, and Paolo Torrini. 2014. “Reusable Components of Semantic Specifications.” In Proceedings of the 13th International Conference on Modularity, April 22-25, 2014, Lugano, Switzerland. ACM.
Lucanu, Dorel, and Traian Florin Serbanuta. 2013. “CinK – an Exercise on How to Think in K.” TR 12-03, Version 2. Alexandru Ioan Cuza University, Faculty of Computer Science. https://fmse.info.uaic.ro/publications/181/.
Lucanu, Dorel, Traian Florin Serbanuta, and Grigore Rosu. 2012. “K Framework Distilled.” In 9th International Workshop on Rewriting Logic and Its Applications, 7571:31–53. LNCS. Springer. http://fsl.cs.illinois.edu/index.php/K_Framework_Distilled.
Mosses, Peter D. 2008. “Component-Based Description of Programming Languages.” In Visions of Computer Science, Proc. BCS International Academic Research Conference, London, UK, 22–24 September 2008, 275–286. Electr. Proc. BCS. http://www.bcs.org/server.php?show=ConWebDoc.22912.