Introduction to the K Framework

Getting started with the K framework

1. Introduction

The K Language Semantic Framework K [1] is a rewriting/reachability based framework for defining executable semantic specifications of programming languages. Given the syntax and semantics of a language, K automatically generates a parser, an interpreter, as well as formal analysis tools such as a deductive verifier. This avoids duplication while improving efficiency and consistency. For example, using the interpreter, one can test the semantics immediately, which significantly increases the efficiency of and confidence in semantics development. There exists a rich literature on using K for formalizing existing languages, such as C [2,3], Java [4] and JavaScript [5], among others. However, as of this writing there are very few literature on the K framework targeting beginners and/or using one of the recent versions -- making the official documentation almost obsolete because people have to lose many hours trying to find a solution to some common issues. This document is an attempt to solve this problem by providing updated step by step instructions targeting beginners on how to install, use and master the K Framework.

2. Introduction to the K Framework

The K framework enables language developers to formally define all programming languages. Once a language is formally specified in the K framework, the framework automatically outputs a range of formal verification tool sets, compilers, debuggers and other developer tools for it. Updates to the language can be made directly in K.

---

This technology has massive implications for smart contract programming language development, and formal verification efforts in the blockchain space. In the past few years, we witnessed the development of multiple smart contract languages - Solidity, Viper, Michelson, Scilla, etc. These languages need to enable developers to write correct, predictable behavior smart contract code. Each language development effort therefore ends up spending resources into building formal verification tool sets, compilers, debuggers and other developer tools.

3. Installation

Installing the K framework is easy as following the instructions given on the release page: https://github.com/kframework/k/releases/latest

We tend to prefer to use the docker images approach.

docker run -it runtimeverificationinc/kframework-k:ubuntu-bionic-master

We can synchronise a folder on the host machine with the /usr/src folder in the container by using a volume:

docker run -it -v "$(pwd)":/usr/src runtimeverificationinc/kframework-k:ubuntu-bionic-master

4. Code editor

We use VS Code as code editor but feel free to use whatever code editor you want.

Depending on your code editor, you may have an extension providing syntax highlighting and code snippets for the K framework.

WIth VS Code, we use the K Language Support Extension from Lucian Cumpata

Note that the same thing can be achieved using any modern code editor: Sublime Text, Atom, etc.

5. Backus-Naur Form (BNF)

This section introduces the concept of a context-free grammar which is a form of grammar ideally suited to describing the syntax of programming languages. The notation typically used to describe such grammars is Backus-Naur Form or BNF which was first used to describe the ALGOL 60 programming language. Backus and Naur are the names of the two individuals who developed and refined this particular form of presentation.

Let’s start off with an example. Here’s a single grammar rule:

<digit> -> 0|1|2|3|4|5|6|7|8|9

The digit is the left-hand side and the part to the right of the arrow is the right-hand side.

Each of the individual numbers (0,1,2,3,4,5,6,7,8,9) are terminals. In the language of grammars they are also called lexemes. The left-hand side is always a non-terminal though we’ll also see some non-terminals on the right-hand side in a moment.

Non-terminals have these angle brackets (<>) around them indicating that they can be expanded into something else.

The vertical bar indicates “or”, so what this rule says is that the entity named digit can transform into a 0 or a 1 or a 2 or so on. Basically any of the digits.

Terminals are aspects of the grammar that cannot be simplified any further. So this rule defines a single digit but what if we want to define numbers consisting of multiple digits. Well, this next example will be another rule and it will use a non-terminal on the right-hand side and in fact it will be a recursive rule.

<digit> -> 0|1|2|3|4|5|6|7|8|9

<nat> -> <digit>

| <digit><nat>

So now our grammar has two rules or productions or production rules as they are sometimes called. We have one rule for digit and another rule for nat which we are using to represent natural numbers. Natural numbers are integers from 0 and up. Basically the non-negative integers. So a natural number can be one of two things, notice we still have the vertical bar but because this wouldn’t fit nicely on one line, the vertical bar is starting the new line, but it still means “or”, so a nat is either a digit which is a non-terminal but we can find out what digit it is by looking at the first rule or a nat is a digit followed by a nat. So nat is defined recursively in terms of itself. The first case with only the digit is a base case and the second case where nat is called again is a recursive case.

These two rules allow us to create numbers of arbitrary length as shown by the following derivation. Derivation starts with a given non-terminal and then expands it one step at the time according to the rules. Now we can

...