K tool, version 3.0
K is a framework for programming language design and executable semantics.
This distribution contains a tool prototype which implements many of K's
features. For more on the K framework and how to use the current tool,
go to k/tutorial (start with the README file there).
NOTE: This README file contains information regarding the stable release of
the K tool indicated in the title above, regardless of whether it came with
the release itself or with subsequent nightly/latest builds. This file is
updated only when new stable versions are officially released.
WARNING: The command line options for kompile, krun, kast and ktest have
recently (starting with version 'jenkins-k-framework-git-359') changed!
Type --help with any of these to see the new options. A list of changes is
here: https://github.com/kframework/k/wiki/Command-Line-Option-Changes.
What is new (from v2.7)
-----------------------
* The front-end is now implemented completely in Java (previously it was
implemented in a combination of Perl and Maude), making use of SDF (as
distributed with the Spoofax system).
Because the parser has changed, the syntax of K definitions has changed, too:
1. Modules and files:
require "filename.k" // require the contents of another file found in the
// current directory, or the 'include' directory.
module MODULE-NAME
imports INCLUDED-MODULE
endmodule // in one word
2. Use priorities instead of precedence:
| Exp "*" Exp
> Exp "+" Exp
3. Binary mixfix operators can be disambiguated with associativity attributes:
syntax Exp ::= Exp "*" Exp [left]
> left:
Exp "+" Exp [left]
| Exp "-" Exp [left]
> non-assoc:
Exp "=" Exp [right]
4. You can use bracket productions to override priorities:
| "(" Exp ")" [bracket]
5. The scope of a variable in k3 is restricted to each rule. In k2 it was the
module. As a result, the sort of each variable should be specified in each
rule in which it is used. If not specified, it is automatically assumed K.
6. The only accepted comments are // ... for one line comments and /* ... */
for multiline ones. Latex comments remain the same:
//@ ...
/*@ ... */
//! ...
/*! ... */
Developers
----------
See src/README