Zdůvodnění
Kontrola, kterou příkaz volá jménem, je vynucování, které nikdo nedeklaroval; dispatcher čte deklarovaná pravidla, takže pravidlo tam přidané běží od té chvíle a to, jehož validátor chybí, selže v doctoru. Stejný argument platí o krok dál: pravidlo dokázané behaviorálním případem, jehož jméno stojí jen anglicky v sekci Verification, je vztah, který nic nedrží — případ lze přejmenovat a pravidlo se dál čte jako dokázané.
Požadované chování
Pravidlo, které nástroj vynucuje, deklaruje blok x-majordomus v režimu odpovídajícím tomu, jak je vynucováno. Pravidlo, které spouští příkaz, je dispatchované: jmenuje validátor mj_validate_<name> s kategorií, návratovým kódem a vynucujícími příkazy, které dispatcher potřebuje. Pravidlo, které dokazuje kontrola, je gated: jmenuje testy a žádný validátor a nic ho nedispatchuje. V obou případech jmenuje alespoň jeden test. Žádný příkaz nevybírá kontroly ručně a žádné pravidlo nestanoví svůj důkaz jen v próze.
Chování při selhání
Loader odmítne blok, který není ani jedním režimem, a pojmenuje chybějící polovinu; množina se nevyřeší. Odeslané pravidlo, jehož validační funkce chybí, selže v doctoru. Blokující pravidlo, které nepojmenovává žádný důkaz, je nový dluh, který scripts/ci/rule-proof-check odmítne, a pravidlo pojmenovávající test, který ve stromu není, selže rovnou, protože takové pravidlo se čte jako dokázané a není.
Ověření
majordomus doctor prochází odeslaný řetězec; test/cases/18_doctrine_wiring.sh jej testuje mutacemi rozbitím každého článku. scripts/ci/rule-proof-check drží kontrolovaný vztah a test/cases/125_rule_proof.sh testuje mutacemi oba režimy, odmítnutí poloviční deklarace loaderem a rohatku.