Uzasadnienia zapewnienia

Uzasadnienie zapewnienia to argument zespołu, że system jest wystarczająco dobry do określonego użycia: każde twierdzenie, jego użycie i dowody, na których się opiera. Uzasadnienie leży obok polityki wydań, w assurance.yaml, więc przechodzi przegląd w pull requestach, a Oloproof czyta każde twierdzenie względem dowodów, które posiada. Nigdy nie mówi, że twierdzenie zostało udowodnione: mówi, które twierdzenia opierają się na aktualnych dowodach z wynikiem pozytywnym, które na dowodach z wynikiem negatywnym, nieaktualnych lub brakujących, a które wyłącznie na założeniach.

Pisanie uzasadnienia

version: 1
goals:
  - id: G1
    statement: The assistant routes tickets well enough for first-line support
    scope: first-line support tickets in English
    strategy: argue over label accuracy and the misrouting hazard
    reassess_when: [the model changes, a new language is supported]
    goals:
      - id: G1.1
        statement: Labels are accurate
        evidence:
          - rule: label-floor
      - id: G1.2
        statement: Misrouting stays rare
        evidence:
          - hazard: missed-label
          - record: records/release-42.json
        defeaters:
          - id: D1
            statement: Tickets in other languages misroute
            resolved_by:
              - rule: label-floor
                suite: multilingual
      - id: G1.3
        statement: The deployment runs the model that was evaluated
        assumptions: [the model is pinned by digest in the deployment manifest]

Cel to twierdzenie. Cel najwyższego poziomu podaje swój scope, czyli zamierzone użycie, dla którego jest formułowany; podcel go dziedziczy. strategy opisuje słowami, jak podcele uzasadniają cel. Każdy element evidence wskazuje dokładnie jedno z:

• rule: reguła z release.yaml, czytana przy ostatnim przebiegu każdego systemu na każdym zestawie; system i suite zawężają, które przebiegi się liczą;
• hazard: zagrożenie z hazards.yaml (Rejestr zagrożeń);
• proof: własność formalna, czytana tak, jak czyta ją reguła dowodowa (Dowody formalne): ostatni wynik otrzymany dla tej własności, przy czym DISPROVED tego samego modelu wygrywa; model (skrót) zawęża ją do jednego sformalizowanego modelu; dopóki projekt nie posiada wyniku, odnośnik niczego nie wspiera;
• record: plik rekordu decyzji zapisany przez oloproof record export, ze ścieżką względem katalogu głównego projektu.

assumptions to to, co cel przyjmuje za pewnik. defeater to powód, dla którego cel może być fałszywy; pozostaje otwarty, dopóki każdy element dowodów z jego resolved_by nie zostanie uznany za wspierający. reassess_when mówi, co powinno skłonić zespół do ponownego przyjrzenia się celowi.

Sprawdzanie

oloproof assurance check

Sprawdzenie odrzuca uzasadnienie, które wymienia regułę nieobecną w polityce albo zagrożenie nieobecne w rejestrze, lub którego cel najwyższego poziomu nie podaje zakresu, i kończy się kodem 2. W przeciwnym razie wypisuje drzewo, a przy każdym celu jeden z czterech statusów:

• supported: wspiera go każdy element jego dowodów i każdy podcel, na aktualnych dowodach, a żaden kontrargument nie jest otwarty;
• undermined: część dowodów ma wynik negatywny, jest nieaktualna lub zaprzeczona, któryś podcel jest podważony albo kontrargument jest otwarty;
• assumptions_only: nic go nie wspiera, a opiera się na podanych założeniach;
• unsupported: każdy inny przypadek, z nazwaniem każdej luki. Cel, który ma pewne wsparcie i jakąś lukę, jest niewspierany: twierdzenie jest tak mocne, jak najsłabsza rzecz, na której się opiera.

Reguła wspiera cel, gdy każdy ostatni przebieg, który ją rozstrzygnął, mówi PASS, i podważa go, gdy którykolwiek mówi FAIL; INSUFFICIENT_EVIDENCE i MANUAL_REVIEW niczego nie wspierają. Zagrożenie wspiera cel, gdy przechodzi każda reguła, która je mierzy. Wynik formalny wspiera cel, gdy własność ma status PROVED, i podważa go, gdy ma status DISPROVED albo gdy dwa wyniki dla jednego modelu się nie zgadzają; wynik mówi, co dowodzi o sformalizowanym modelu, nigdy o wdrożeniu. Rekord wspiera cel, gdy skrót jego treści nadal równa się jego identyfikatorowi, a jego decyzja to PASS. Dowody z przebiegu, który nie pasuje już do projektu (zmienił się jego system, zestaw, ewaluatory lub polityka), są nieaktualne i podważają cel. Te statusy należą do uzasadnienia, nigdy nie są decyzjami i nigdy nie zmieniają kodu wyjścia. --json zapisuje ten sam raport dla potoku.

Gdzie się pojawia

oloproof run zapisuje uzasadnienie razem z przebiegiem, oloproof push przenosi uzasadnienie przebiegu do twojej przestrzeni roboczej wraz z wynikami formalnymi, które wskazują jego odnośniki do dowodów, a oloproof export zapisuje jego odczyt przez silnik obok pakietów. Strona Safety and risk pokazuje drzewo z każdym statusem tak, jak zapisał go silnik, a każda reguła ma odnośnik do swoich dowodów. W przestrzeni roboczej uzasadnienie jest czytane względem przebiegów, które wypchnąłeś: aktualność nie jest tam porównywana, bo nie ma pliku projektu, z którym można by ją porównać, a odnośniki do rekordów czyta tylko oloproof assurance check. Rekord decyzji wymienia uzasadnienie zapisane przez jego przebieg; record verify przedstawia je jako słowo zespołu.

Co dalej

• Rejestr zagrożeń opisuje zagrożenia, na których może opierać się cel.
• Graf dowodów rysuje każde twierdzenie razem z dowodami, na których się opiera.