K Framework Documentation

K is a framework designed for formal language definition. By defining a language formally in K, you can automatically extract a suite of tools for that language, including:

• Interpreters
• Parsers
• Symbolic verifiers

This tutorial is intended for developers with a strong computer science background and experience in functional programming languages.

SIMPLE is a pedagogical and research language designed to capture the essence of the imperative programming paradigm. It is implemented as a K semantic definition.

Key features include:

• Multidimensional arrays: Arrays evaluate to array references (location + size) and can be stored in variables.
• Functions: Supports zero or more parameters, call-by-value parameter passing, static scoping, and abrupt returns via return.
• Blocks with locals: Variables can be declared within blocks, with scope extending to the end of the most nested enclosing block.
• Input/Output: Uses read() to pull from an input buffer and write(e) to push to an output buffer.
• Exceptions: Supports parametric exceptions.
• Concurrency: Supports dynamic thread creation/termination, synchronization via join, re-entrant locks, and rendezvous commands.

The K Framework provides several command-line interface (CLI) tools that revolve around K specifications. These tools are categorized by their primary function:

• Transforming K Specs: kompile is the K compiler driver used to transform a K specification into an intermediate representation called Kore.
• Running K Specs: krun is the interpreter and symbolic execution engine driver used for concrete and abstract execution.
• Parsing and AST Transformation: kparse is a standalone K parser and abstract syntax tree (AST) transformation tool.
• Analyzing K Specs: kprove is the K theorem prover used for verifying claims about a K specification.

IMP++ is an extension of the IMP language designed for use with the K framework. Key features include:

• Strings: Supports string concatenation using the + operator.
• Variable Increment: Includes a pre-increment construct ++x which has side effects on expression evaluation.
• I/O: Adds read() to read integers and a variadic print(e1, e2, ..., en) statement.
• Abrupt Termination: The halt statement stops the current thread.
• Dynamic Threads: The spawn s expression starts a new concurrent thread executing statement s, returning a fresh thread identifier. Threads can synchronize using join t;.
• Blocks and Local Variables: Supports curly-bracketed blocks { ... } and allows variable declarations anywhere, with scope limited to the enclosing block.

This section of the tutorial is designed for developers who have already gained a basic understanding of K and wish to master less commonly-used features. Completing these lessons enables a developer to read and understand most K specifications, write complex specifications, and perform common K-related tasks.

Each lesson is independent and covers a specific facet of the language. For exhaustive technical details beyond these tutorials, refer to the User Manual.

K is a framework for defining programming languages. A language definition in K consists of two primary components:

1. Syntax: Defined using a BNF-style notation (enriched with features to support semantics). This specifies how programs in the language are structured.
2. Semantics: Specifies what each language construct does and how it executes.

By providing a formal, rigorous definition, K automatically provides a suite of tools for that language, including:

• A parser
• An interpreter
• A state-space explorer (for reachability model-checking)
• A deductive program verifier

K is an executable semantic framework used to define programming languages, calculi, type systems, and formal analysis tools. It is designed to handle concurrent languages (even with sharing) and control-intensive features like exceptions, abrupt termination, or call/cc.

Because K treats computations as terms in a rewriting environment, you can match, move, modify, or delete them. A single semantic definition in K can be used to automatically generate several tools, including:

• Interpreters
• Debuggers
• State space search engines
• Model checkers

In dynamically typed SIMPLE, every location is assigned a type that cannot change during program execution. The undefined(Type) construct is used to initialize a location with both a specific type and an undefined value. Each location corresponds to an allocated variable or array element.

Key semantic behavior:

• undefined(Type) assigns a type and an undefined value to a location.
• Locations are not reclaimed or reused in this semantic definition.

  syntax KItem ::= undefined(Type)

  rule <k> T:Type X:Id; => .K ...</k>
       <env> Env => Env[X <- L] </env>
       <store>... .Map => L |-> undefined(T) ...</store>
       <nextLoc> L:Int => L +Int 1 </nextLoc>

To ensure an expression is an lvalue (something that can be assigned to, like an Id), use the ltype context. Because context ltype(HOLE:LValue) may fail due to internal errors, the recommended pattern is to use a context with a requires clause checking an isLValue predicate.

  syntax LValue ::= Id
  rule isLValue(_:Exp[_:Exps]) => true
  syntax Exp ::= LValue

  syntax Exp ::= ltype(Exp)
  context ltype(HOLE) requires isLValue(HOLE)