Eine Regel ist eine Formel mit Version.

Was gebaut ist

Eine Regel hält fest, was gelten muss, bevor eine Handlung wirkt. In KALKÜL ist sie zugleich der Wortlaut einer Vorschrift und eine Formel, die ein Löser prüfen kann. Dieser geplante Vertrag legt fest, was zu einer Regel gehört, damit Wortlaut und Formel nicht auseinanderlaufen und jede Prüfung auf eine bestimmte Fassung zeigt.

Ein geplanter Vertrag, kein erreichbarer Endpunkt

Die Felder beschreiben die vorgesehene Form einer Regel. Der Demonstrator von KALKÜL rechnet im Browser mit drei festen Regeln im Quelltext, Sperrraum, Obergrenze und Reserve; ein Anlegen, Versionieren und Prüfen von Regeln über eine Schnittstelle besteht nicht.

Wortlaut und Formel gehören zusammen

Eine Regel trägt ihren Wortlaut, ihre Fundstelle in der Vorschrift und die Formel, die ihn ausdrückt. Die Formel steht in SMT-LIB, dem gemeinsamen Format der Löser, über benannten Variablen mit Typ, Einheit und Bereich. Erst wenn Fachleute für eine Reihe von Zuständen mit bekannter Antwort bestätigt haben, dass die Formel dasselbe sagt wie der Wortlaut, geht die Version in Betrieb.

Version und Geltung

Begriff · Nachweis

Der signierte Datensatz einer Prüfung: Handlung, Zustand, Regeln, Ergebnis und Voraussetzungen, mit Prüfwert, Signatur und Zeitstempel. Er lässt sich ohne Zugang zum System nachrechnen.

Nachweis im Zusammenhang

Eine Regel ändert sich nur durch eine neue Version. Jede Prüfung und jeder Nachweis nennt die Fassung, gegen die gerechnet wurde. Eine Version hat einen Gültigkeitszeitraum, einen Verantwortlichen und einen Verweis auf die Vorgängerin. Sie wird nie überschrieben, damit eine spätere Prüfung genau die Regel von damals findet.

Harte und weiche Regeln

Eine harte Regel bricht nie, höchstens mit einer Ausnahme und Freigabe. Eine weiche Regel ist eine Vorliebe mit Gewicht, die eine Optimierung abwägt. Die Art steht an der Regel. Dieselbe Regel gilt für die Prüfung und für die Optimierung.

Testfälle gehören zur Regel

Eine Regel ohne Testfälle wird nicht aktiv. Die Testfälle sind Zustände mit der Antwort, die die Regel liefern muss, und laufen bei jeder neuen Version. Ein Satz von Regeln wird außerdem auf Widerspruch geprüft: Lässt er keinen Zustand zu, meldet das System die kleinste Menge von Regeln, die einander ausschließen.

Schema

regel: <kennung>
version: <nummer>
art: hart | weich
wortlaut: "<text der vorschrift>"
fundstelle: <vorschrift, absatz>
variablen:
  <name>: { typ: real, einheit: <einheit>, bereich: [<von>, <bis>] }
formel: "(=> (not <freigabe>) (>= <groesse> <grenze>))"
gueltig_von: <datum>
verantwortlich: <rolle>
tests: [<testfall>, <testfall>]

Schema 1YAML · Schema mit Platzhaltern

Felder

Feld	Typ	Pflicht	Bedeutung
`id`	`string`	ja	Stabile Kennung der Regel über alle Versionen.
`version`	`integer`	ja	Fassung der Regel. Wird nie überschrieben, nur durch eine neue ersetzt.
`kind`	`string`	ja	hard oder soft. Weiche Regeln tragen ein Gewicht und gehen in das Ziel einer Optimierung ein.
`wording`	`string`	ja	Wortlaut der Vorschrift, wie er in der Quelle steht.
`citation`	`string`	ja	Fundstelle der Vorschrift mit Absatz.
`variables`	`object[]`	ja	Variablen mit Typ, Einheit und Bereich. Unbekannte Variablen in der Formel werden zurückgewiesen.
`formula`	`string`	ja	Formel in SMT-LIB über den Variablen. Muss den Wortlaut ausdrücken.
`weight`	`number`	nein	Gewicht einer weichen Regel. Fehlt bei harten Regeln.
`validFrom`	`string (date)`	ja	Beginn der Geltung. Ende nur, wenn die Vorschrift endet.
`owner`	`string`	ja	Verantwortliche Rolle für Inhalt und Übersetzung.
`supersedes`	`integer`	nein	Nummer der abgelösten Version.
`tests`	`string[]`	ja	Verweise auf Testfälle. Ohne Testfälle wird die Regel nicht aktiv.

Fehlerfälle

Kennung	Bedeutung
`RULE_FORMULA_INVALID`	Die Formel ist kein gültiger Ausdruck in SMT-LIB oder verwendet eine nicht unterstützte Theorie.
`RULE_VARIABLE_UNKNOWN`	Die Formel nennt eine Variable, die nicht unter variables steht.
`RULE_TESTS_FAILED`	Die Formel liefert für einen Testfall nicht die erwartete Antwort; die Version wird nicht aktiv.
`RULE_SET_CONTRADICTORY`	Die aktiven Regeln lassen keinen Zustand zu; die kleinste widersprüchliche Menge wird genannt.
`RULE_VERSION_CONFLICT`	Die neue Version beruht auf einer überholten Fassung.

Grenze

Grenze: Dieser Schnittstellenvertrag ist geplant. Er belegt weder eine veröffentlichte Schnittstelle noch eine fachliche Übersetzung einer Vorschrift; ob eine Formel den Wortlaut richtig wiedergibt, bleibt Sache der fachlichen Prüfung.

Quellen

SMT-LIB: The Satisfiability Modulo Theories LibraryGemeinsames Eingabeformat der Löser und Beschreibung ihrer Theorien.