Skip to content

README.de.md

Latest commit

 

History

History
129 lines (94 loc) · 8.96 KB

README.de.md

File metadata and controls

129 lines (94 loc) · 8.96 KB
Raw

English · Español · Português · Deutsch · Français · 简体中文 · 繁體中文 · 한국어 · 日本語 · Русский · Türkçe

proofreader-skill

proofreader-skill

Eine allgemeine Korrektur-Skill, geschrieben nach dem offenen Agent-Skills-Standard (SKILL.md-Format). Einfach in jedes Tool legen, das den Standard unterstützt (Claude Code, Codex CLI, Gemini CLI usw.), und direkt verwenden.

Das werkzeugübergreifende Laden wurde empirisch mit Codex CLI getestet: Anhand seiner Liste installierter Skills wählte es für eine ACSL-Korrekturaufgabe korrekt proofreader-skill aus und zitierte dabei die genauen Trigger-Schlüsselwörter aus dem description-Feld von SKILL.md. Die Kompatibilität mit anderen Tools ergibt sich daraus, dass skills-ref validate (die offizielle Prüfung der Agent-Skills-Spezifikation) besteht, wurde aber nicht Tool für Tool einzeln getestet.

Dieses README ist die menschenlesbare Projektbeschreibung. Das tatsächliche Verhalten der KI wird durch SKILL.md und die Detaildokumente unter references/ gesteuert.

Was diese Skill macht

Zwei parallele, gleichermaßen wichtige Fähigkeiten:

  1. Code-Korrektur — allgemeine Prüfung der Code-Logik (beliebige Sprache), plus dedizierte Backends für formale Verifikation bestimmter Sprachen:
    • C + ACSL: Das WP-Plugin von Frama-C erbringt den statischen Beweis von ACSL-Verträgen (requires/ensures/assigns/Schleifeninvarianten usw.); E-ACSL übersetzt dieselben Annotationen in Laufzeitprüfungen, die während der tatsächlichen Ausführung geprüft werden — eine Verletzung liefert ein konkretes Gegenbeispiel
    • Python: icontract-Dekoratoren prüfen Verträge zur Laufzeit; CrossHair führt symbolische Ausführung durch, um ein Gegenbeispiel zu suchen (eine begrenzte Suche, kein erschöpfender Beweis)
    • Rust: Kani (bounded model checking) verifiziert ein #[kani::proof]-Harness — erschöpfend für schleifenfreien Code, begrenzt bei Schleifen/Rekursion, sofern das Unwind-Limit nicht passend gesetzt ist
    • Java: JML-Verträge (//@ requires/ensures, das JML-Äquivalent zu ACSL) werden mit dem statischen Prüfer -esc von OpenJML verifiziert
    • C++: CBMC (bounded model checking; es gibt kein ausgereiftes "ACSL für C++") — dieselbe Werkzeugfamilie wie Kani, direkt auf C/C++ angewendet
  2. Dokumentenkorrektur — Grammatik-, Terminologiekonsistenz-, Logikkonsistenz- und Formatierungsprüfungen für mehrsprachige Texte/Dokumente

Details zur Routing-Logik siehe SKILL.md.

Verzeichnisstruktur

SKILL.md                          Einstiegspunkt: Klassifizierungs-Routing (Code/Dokument; Code wird zusätzlich zum passenden sprachspezifischen Verifikations-Backend weitergeleitet)
references/
  code-proofreading.md            Allgemeine Methodik zur Prüfung der Code-Logik
  acsl-frama-c.md                 ACSL-Vertragsprüfung + Nutzung des statischen Beweises Frama-C/WP (C)
  eacsl-runtime.md                Nutzung der E-ACSL-Laufzeitverifikation (C)
  python-contracts.md              icontract-Vertragsprüfung + Nutzung von CrossHair (Python)
  rust-kani.md                     Nutzung des Kani bounded model checking (Rust)
  java-openjml.md                  JML-Vertragsprüfung + Nutzung von OpenJML `-esc` (Java)
  cpp-cbmc.md                       Nutzung des CBMC bounded model checking (C++)
  doc-proofreading.md             Methodik zur Korrektur mehrsprachiger Dokumente
examples/
  abs-int/                        C+ACSL-Fallstudie (WP- + E-ACSL-Ausgabe ist echt, tatsächlich ausgeführt)
  python-contracts/                 Fallstudie Python + icontract/CrossHair
  rust-kani/                        Fallstudie Rust + Kani
  java-openjml/                     Fallstudie Java + JML/OpenJML
  cpp-cbmc/                          Fallstudie C++ + CBMC
  code-proofreading/               Fallstudie zur allgemeinen Code-Korrektur
  doc-proofreading/                Fallstudie zur Dokumentenkorrektur
scripts/
  verify.sh                       Regressionsprüfung: führt die obigen Fallstudien erneut aus, um Abweichungen zwischen Dokumentation und tatsächlichem Tool-Verhalten zu erkennen

Verwendung

Der npx skills add-Weg unten setzt voraus, dass dieses Repository zuerst in einem öffentlich zugänglichen Git-Repository (z. B. GitHub) veröffentlicht wird. Solange es noch nicht zu einem Remote gepusht wurde, nutze die manuelle Installation per Clone/Kopie.

Ein-Schritt-Installation (empfohlen, tool-übergreifend) — über die Vercel-skills-CLI:

npx skills add <owner>/proofreader-skill -a claude-code
# unterstützte -a-Ziele umfassen claude-code, opencode usw. — die aktuelle Liste findest du in der skills-CLI-Dokumentation

Manuelle Installation: Das gesamte Repository in das Skills-Verzeichnis legen, das dein Tool erwartet. Der Verzeichnisname muss proofreader-skill bleiben (die Agent-Skills-Spezifikation verlangt, dass das name-Feld in SKILL.md mit dem übergeordneten Verzeichnisnamen übereinstimmt; prüfbar mit npx skills-ref validate <path>):

# Claude Code
cp -r proofreader-skill ~/.claude/skills/proofreader-skill

# Codex CLI / andere SKILL.md-kompatible Tools
# folge der jeweiligen Skills-Verzeichniskonvention dieses Tools und behalte den Verzeichnisnamen bei

Die Backends für formale Verifikation einrichten

Jedes sprachspezifische Backend braucht seine eigene Toolchain. Vollständige, tatsächlich ausgeführte Installations- und Verifikationsprotokolle stehen im README der jeweiligen Fallstudie — echte Befehle und echte Ausgaben, keine Beschreibung des erwarteten Verhaltens.

C (Frama-C / E-ACSL) — siehe references/acsl-frama-c.md, references/eacsl-runtime.md, examples/abs-int/README.md. Kurzfassung (über opam, nicht apt — der apt-Index eines frischen Ubuntu 22.04 enthält das Paket frama-c möglicherweise nicht):

sudo apt-get install -y opam libgmp-dev libgtksourceview-3.0-dev
opam init -y --disable-sandboxing --bare
opam switch create frama-c 4.14.1
eval $(opam env --switch=frama-c)
opam install -y --assume-depexts frama-c
why3 config detect   # zwingend erforderlich — sonst schlägt WP mit "Prover 'Alt-Ergo' not found" fehl

Python (icontract / CrossHair) — siehe references/python-contracts.md, examples/python-contracts/README.md:

pip3 install --user crosshair-tool icontract

Rust (Kani) — siehe references/rust-kani.md, examples/rust-kani/README.md:

cargo install --locked kani-verifier
cargo kani setup

Java (OpenJML) — siehe references/java-openjml.md, examples/java-openjml/README.md. Wähle den Release-Build passend zur glibc/Distribution deines Systems (neuere Releases liefern nur noch einen Ubuntu-24.04-Build; ältere hatten auch einen für 22.04) — prüfe, ob openjml --version tatsächlich eine OpenJML-Version ausgibt und nicht einfach eine normale javac-Version, bevor du der Ausgabe vertraust:

curl -fsSL -o openjml.zip https://github.com/OpenJML/OpenJML/releases/download/<version>/openjml-<your-distro>-<version>.zip
unzip openjml.zip -d openjml && cd openjml
./openjml --version

C++ (CBMC) — siehe references/cpp-cbmc.md, examples/cpp-cbmc/README.md. Entweder apt-get install cbmc (braucht sudo), oder das Release-.deb für deine Distro ohne Root entpacken:

curl -fsSL -o cbmc.deb https://github.com/diffblue/cbmc/releases/download/<version>/<your-distro>-cbmc-<version>-Linux.deb
dpkg-deb -x cbmc.deb ./cbmc-local
export PATH="$PWD/cbmc-local/usr/bin:$PATH"

Status

  • Die Routing-Logik von SKILL.md und alle Dokumente unter references/ sind fertig; das Frontmatter von SKILL.md besteht die offizielle skills-ref validate-Prüfung
  • Jeder Bereich (C+ACSL, Python, Rust, Java, C++, allgemeine Code-Korrektur, Dokumentenkorrektur) hat mindestens eine echte, verifizierte Fallstudie unter examples/
  • scripts/verify.sh bietet eine Regressionsprüfung, die die obigen Fallstudien erneut ausführt und mit den festgehaltenen erwarteten Ergebnissen vergleicht

Issues und PRs sind willkommen.

Lizenz

MIT