ACSL (ANSI/ISO C Specification Language) ist eine formale Spezifikationssprache für C-Programme, entwickelt im Frama-C-Projekt. Ihr Design ist von JML (Java Modeling Language) inspiriert und erbt viel von Caduceus, einem früheren Analysewerkzeug. Mit ACSL beschreibt man das Verhalten von C-Funktionen präzise — als Verträge mit Vorbedingung, Nachbedingung und Frame-Regel — und lässt diese Eigenschaften anschließend maschinell beweisen.
Syntax: Annotationen als Kommentare
/*@ requires n >= 0;
@ ensures
esult == n * (n + 1) / 2;
@ assigns
othing;
@*/
int summe(int n) {
int s = 0;
/*@ loop invariant 0 <= i <= n && s == i * (i - 1) / 2;
@ loop assigns s, i;
@ loop variant n - i;
@*/
for (int i = 1; i <= n; i++) s += i;
return s;
}Wichtige Konstrukte
requires— Vorbedingung (Precondition), die der Aufrufer garantieren muss.ensures— Nachbedingung (Postcondition), die die Funktion garantiert.assigns— Frame-Regel: welche Speicherbereiche die Funktion verändern darf.loop invariant/loop variant— Schleifeninvariante und Terminierungsargument.
Logische Terme
ACSL stellt spezielle Terme bereit:
esult (Rückgabewert), old(ausdruck) (Wert vor dem Funktionsaufruf), valid(zeiger) (gültiger Speicherbereich), valid_range, length,
othing (leere Frame-Regel),
ull, rue/false.
Einordnung
ACSL wird von den Frama-C-Plugins verarbeitet: WP (Weakest Precondition) erzeugt Beweisverpflichtungen, die Why3 an Beweiser wie Alt-Ergo oder Z3 delegiert; EVA analysiert mit abstrakter Interpretation; E-ACSL übersetzt Annotationen in Laufzeitprüfungen. Damit steht ACSL in einer Reihe mit anderen formalen Spezifikationssprachen: VDM und Z-Notation spezifizieren auf höherer Ebene, HOL-Assistenten können die erzeugten Verpflichtungen interaktiv beweisen.
Verwandte Grundlagen: Frama-C-Befehle, Why3-Befehle, C/C++-Befehle.