CinK in Funcons

Peter D Mosses
Ferdinand Vesely

Department of Computer Science, Swansea University

January 2014

Introduction

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.

To produce a prototype implementation of language L

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.

To run an L-program P

    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.

Languages

Each language specification consists of the following files:

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

Expressions

This pure expression sub-language includes only integer and boolean literals, unary and binary operators, and conditional conjunction and disjunction.

Declarations

This sub-language adds variable declarations, and extends expressions with identifiers, assignments and the comma operator.

Statements

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

Functions

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

Threads

This extension provides only very basic language support for spawning threads.

Compare to previous sub-language: semantics | syntax

References

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

Pointers

Variable declarations and expressions are extended to support pointers.

Compare to previous sub-language: semantics | syntax

Funcons

The K specifications of all the funcons, each in a separate file:

Funcon sorts

Individual funcons

Values

The K specifications of all the data types of values, each in a separate file:

Acknowledgments

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

References

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.