K-Framework

Install

Used Docker to execute the K framework (Available at the runtimeverification/kframework-k Docker Hub repository.)

To download the docker image:

docker pull runtimeverificationinc/kframework-k:ubuntu-focal-COMMIT_ID

To run the docker image:

docker run -it runtimeverificationinc/kframework-k:ubuntu-focal-COMMIT_ID

A K file (with .k extension) consists of one or more requires or modules.
Each module consists of one or more imports or sentences.
K’s compiler is called kompile, compiles it into an interpreter
A set of K files that are compiled together are called a K definition.
krun will use the interpreter generated by the first call to kompile to execute this program.
A rule begins with the rule keyword and contains at least one rewrite operator (=>).
K’s grammar is divided into two components:
- the outer syntax of K (predetermined): parsing of requires, modules, imports, and sentences in a K definition.
- the inner syntax of K (defined by you, the developer): parsing of rules and programs.