K ist ein Rewrite-basiertes ausführbares semantisches Framework, in dem Programmiersprachen, Typsysteme und formale Analysetools mithilfe von Konfigurationen, Berechnungen und Regeln definiert werden können. Konfigurationen organisieren diestatus in Einheiten, die Zellen genannt werden, die beschriftet sind und verschachtelt werden können.Berechnungen haben eine rechnerische Bedeutung als spezielle verschachtelte Listenstrukturen, die Rechenaufgaben sequentialisieren, z. B. Fragmente von Programmen. Berechnungen erweitern die abstrakte Syntax der Originalsprache.K (rewrite) Regeln machen es explizit, welche Teile des Begriffs theyread-only, write-only, read-write oder sich nicht darum kümmern. Dies macht es geeignet, wirklich gleichzeitige Sprachen auch in Gegenwart von Sharing zu definieren. Berechnungen sind wie alle anderen Terme in einer Schreibumgebung: Sie können abgeglichen, von einem Ort zum anderen verschoben, geändert oder gelöscht werden. Dies macht K geeignet für die definierungsteuerungsintensive Funktionen wie abrupte Beendigung, Ausnahmen orcall / cc.
Übersicht
- Eine zehnminütige Übersichtsvideopräsentation.
- Ein neunzigminütiges Tutorial-Video, gegeben auf der ETAPS’16.
- Ein hochrangiges Interview über Rewrite-basierte Semantik (Wolfram Schulte interviewt Grigore Rosu auf der ICSE’11.
- FAQ
K-Tool herunterladen
- Die bereitgestellten K-Tool-Binärdateien werden unter Linux, OS X und Windows unterstützt. Andere Plattformen funktionieren möglicherweise nicht ordnungsgemäß. Wir freuen uns über Informationen über die Benutzerfreundlichkeit nicht unterstützter Plattformen oder Fehler in den unterstützten Plattformen.
- Auf unserer Editor-Support-Seite finden Sie Links zu K Syntax-Highlighting-Definitionen für verschiedene gängige Editoren/IDEs. Bitte zögern Sie nicht, einen Beitrag zu leisten.
- Der Quellcode (Java) ist auf GitHub verfügbar, wo Sie auch Fehler melden können (bitte tun Sie dies).
Lerne K
- Mach das K-Tutorial!
- Lesen Sie einige Artikel über K im Formal Systems Laboratory (FSL).
- Benutzerdokumentation
- Builtins
Links
- K und passende Logik-Webseite bei UIUC (USA).
- K Webseite bei UAIC (Rumänien).
- Matching logic Webseite bei UIUC (USA).
- Online-K-Diskussionskanal für K-Benutzer (Slack & Riot). Dies ist der empfohlene Weg, um Fragen zu K zu stellen und mit der K-Community zu interagieren.
- Stackoverflow für allgemeine Fragen an die K-Benutzergemeinschaft (verwenden Sie den obigen Kanal, wenn Sie schnelle Antworten wünschen).
