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.
- Examples is available.