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:

• cinf-syntax.k: the language syntax
• cinf.k: rules translating the language syntax to funcons and values
• cinf-<language>-funcons.k: importing the required funcons
• cinf-<language>-values.k: importing the required values

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

• comm – command funcons
• decl – declaration funcons
• expr – expression funcons

Individual funcons

• allocate – variable allocation
• apply – abstraction application
• assign-giving-current-value – assignment expressions giving current value
• assign-giving-variable – assignment expressions giving variables
• assign – assignment commands
• bind-value – binding identifiers to values
• bound-value – identifier bound-value expressions
• catch – catching thrown values
• close – closure construction
• closure – closure evaluation
• current-value – stored value of a variable, identity on other values
• decl-effect – commands as declarations
• effect – effects of expressions
• given – value given by supply
• if-true-comm – conditional commands
• if-true-expr – conditional expressions
• input – input integer from stream
• match-compound – matching compound patterns to compound values
• match – matching patterns to values
• output – output to stream
• reset-env – auxiliary to scoping funcons
• reset-given – auxiliary to supply(E, K)
• scope-comm – scoping declarations in command
• scope-expr – scoping declaration in expression
• seq-comm – sequencing commands
• seq-decl – sequencing command before declaration
• seq-expr – sequencing command before expression
• spawn – thread creation and termination
• stored-value – variable value expressions
• supply-decl – supply value to declaration
• supply-expr – supply value to command
• throw – throwing values
• while-true – while-loop commands

Values

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

• abstractions – abstractions
• bindings – bindings
• booleans – boolean values
• functions – function abstractions
• integers – integer values
• patterns – pattern abstractions
• skip – normal command termination
• streams – streams
• strings – strings
• threads – thread names
• tuples – tuple values
• types – types of values
• unit – unit type
• values – values computed by Expr
• variables – variables
• variants – variant values
• xstacks – xstack items

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