Casi di garanzia

Un caso di garanzia è l'argomentazione del team che un sistema è adatto a un uso dichiarato: ogni affermazione, l'uso per cui è fatta e l'evidenza su cui poggia. Il caso vive accanto alla policy di rilascio, in assurance.yaml, quindi si rivede nelle pull request, e Oloproof legge ogni affermazione rispetto all'evidenza che possiede. Non dice mai che un'affermazione è dimostrata: dice quali affermazioni poggiano su evidenza attuale con esito positivo, quali su evidenza con esito negativo, non aggiornata o mancante, e quali soltanto su ipotesi.

Scrivere il caso

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]

Un obiettivo è un'affermazione. Un obiettivo di primo livello dichiara il suo scope, l'uso previsto per cui è affermato; un sotto-obiettivo lo eredita. strategy dice a parole come i sotto-obiettivi argomentano l'obiettivo. Ogni elemento di evidence nomina esattamente uno tra:

• rule: una regola di release.yaml, letta all'ultima esecuzione di ogni sistema su ogni suite; system e suite restringono le esecuzioni che contano;
• hazard: un pericolo di hazards.yaml (Registro dei pericoli);
• proof: una proprietà formale, letta come la legge una regola di prova (Prove formali): l'ultimo risultato ricevuto per la proprietà, con un DISPROVED dello stesso modello che prevale; model (un digest) la restringe a un solo modello formalizzato; finché il progetto non possiede un risultato, il collegamento non sostiene nulla;
• record: un file di record di decisione scritto da oloproof record export, relativo alla radice del progetto.

Le assumptions sono ciò che l'obiettivo dà per scontato. Un defeater è un motivo per cui l'obiettivo potrebbe essere falso; resta aperto finché ogni elemento dell'evidenza nel suo resolved_by non dà sostegno. reassess_when dice che cosa dovrebbe riportare il team all'obiettivo.

Verificarlo

oloproof assurance check

La verifica rifiuta un caso che nomina una regola assente dalla policy o un pericolo assente dal registro, o il cui obiettivo di primo livello non dichiara alcun ambito, e termina con 2. Altrimenti stampa l'albero, ogni obiettivo con uno di quattro stati:

• supported: ogni elemento della sua evidenza e ogni sotto-obiettivo lo sostengono, su evidenza attuale, e nessuna obiezione è aperta;
• undermined: qualche evidenza fallisce, non è aggiornata o è contraddetta, un sotto-obiettivo è indebolito, oppure un'obiezione è aperta;
• assumptions_only: nulla lo sostiene, e poggia su ipotesi dichiarate;
• unsupported: tutto il resto, con ogni lacuna nominata. Un obiettivo con un certo sostegno e una lacuna non è sostenuto: un'affermazione è forte quanto la cosa più debole su cui poggia.

Una regola sostiene un obiettivo quando ogni ultima esecuzione che l'ha decisa dice PASS, e lo indebolisce quando una qualsiasi dice FAIL; INSUFFICIENT_EVIDENCE e MANUAL_REVIEW non sostengono nulla. Un pericolo sostiene quando ogni regola che lo misura passa. Un risultato formale sostiene quando la proprietà è stata PROVED, e indebolisce quando è stata DISPROVED o quando due risultati per uno stesso modello discordano; un risultato dice che cosa dimostra sul modello formalizzato, mai sul deployment. Un record sostiene quando il suo contenuto ha ancora come digest il suo id e la sua decisione è PASS. L'evidenza di un'esecuzione che non corrisponde più al progetto (il suo sistema, la suite, i valutatori o la policy sono cambiati) non è aggiornata e indebolisce. Questi stati sono del caso, mai decisioni, e non cambiano mai un codice di uscita. --json scrive lo stesso rapporto per una pipeline.

Dove compare

oloproof run registra il caso con l'esecuzione, oloproof push porta il caso dell'esecuzione nel vostro spazio di lavoro con i risultati formali nominati dai suoi collegamenti di prova, e oloproof export scrive accanto ai bundle la lettura che ne fa il motore. La pagina Safety and risk mostra l'albero con ogni stato come l'ha scritto il motore, ogni regola collegata alla sua evidenza. Nello spazio di lavoro il caso è letto rispetto alle esecuzioni che avete inviato: lì la freschezza non viene confrontata, perché non c'è un file di progetto con cui confrontarla, e i collegamenti ai record sono letti solo da oloproof assurance check. Un record di decisione nomina il caso registrato dalla sua esecuzione; record verify lo riporta come parola del team.

Dove andare dopo

• Registro dei pericoli tratta i pericoli su cui può poggiare un obiettivo.
• Grafo delle evidenze disegna ogni affermazione con l'evidenza su cui poggia.