Kは書き換えベースの実行可能なセマンティックフレームワークであり、プログラミング言語、型システム、形式解析ツールを構成、計算、ルールを使用して定義することができる。 構成は、ラベルが付けられ、入れ子にすることができるセルと呼ばれる単位で状態を整理します。計算は、プログラムの断片のような計算タスクをシーケンス化する特別なネストされたliststructuresとして計算の意味を持ちます。 計算は、元の言語の抽象構文を拡張します。K（書き換え）ルールは、用語のどの部分が読み取り専用、書き込み専用、読み取り書き込み、または気にしないかを明示します。 これは、共有の存在であっても真の並行言語を定義するのに適しています。 計算は、arewriting環境の他の用語と同様です：それらは、一致、ある場所から別の場所への移動、変更、または削除することができます。 これにより、Kは突然の終了、例外orcall/ccなどの制御集約的な機能を定義するのに適しています。
概要
- 10分間の概要ビデオスライドプレゼンテーション。
- ETAPS’16で提供された九十分のチュートリアルビデオ。
- 書き換えベースの意味論についてのハイレベルなインタビュー(Wolfram Schulte interviews GRIGORE Rosu at ICSE’11.
- FAQ
Kツールのダウンロード
- 提供されているKツールバイナリは、Linux、OS X、およびWindowsでサポートされています。 他のプラットフォームは正常に動作する場合としない場合があります。 サポートされていないプラットフォームの使いやすさやサポートされてい
- 様々な一般的なエディタ/IdeのK構文強調表示定義へのリンクについては、エディタのサポートページを試してみてください。 自由に貢献してください。
- ソースコード(Java)はGitHubで入手でき、バグを報告することもできます(そうしてください)。
Kを学ぶ
- Kチュートリアルを行います！
- 形式システム研究所（FSL）のKに関するいくつかの論文を読んでください。
- ユーザードキュメント
- 組み込み
リンク
- KとUIUC(米国)のマッチングロジックwebページ。
- KはUAIC（ルーマニア）でwebページを作成しました。
- UIUC（米国）のマッチングロジックwebページ。
- Kユーザー向けのオンラインKディスカッションチャンネル(Slack&Riot)。 これは、Kについての質問をし、Kコミュニティと対話するための推奨される方法です。
- Kユーザーコミュニティへの一般的な質問については、Stackoverflowを使用してください（簡単な回答が必要な場合は、上記のチャネルを使用してください）。
