Argumentaires d’assurance

Un argumentaire d’assurance est la démonstration par votre équipe qu’un système convient à un usage déclaré : chaque affirmation, son usage et sa preuve. L’argumentaire vit à côté de la politique de publication, dans assurance.yaml : il est donc relu en pull request, et Oloproof lit chaque affirmation au regard des preuves qu’il détient. Il ne dit jamais qu’une affirmation est prouvée : il dit lesquelles reposent sur des preuves actuelles qui réussissent, lesquelles sur des preuves en échec, périmées ou manquantes, et lesquelles sur de seules hypothèses.

Rédiger l’argumentaire

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 objectif est une affirmation. Un objectif de premier niveau déclare son scope, l’usage prévu pour lequel il est affirmé ; un sous-objectif en hérite. strategy dit en mots comment les sous-objectifs argumentent l’objectif. Chaque élément d’evidence nomme exactement l’un des suivants :

• rule : une règle de release.yaml, lue à la dernière exécution de chaque système sur chaque suite ; system et suite restreignent les exécutions qui comptent ;
• hazard : un danger de hazards.yaml (Registre des dangers) ;
• proof : une propriété formelle, lue comme une règle de preuve la lit (Preuves formelles) : le dernier résultat reçu pour la propriété, un DISPROVED du même modèle l’emportant ; model (un condensé) la restreint à un seul modèle formalisé ; tant que le projet ne détient aucun résultat, le lien ne soutient rien ;
• record : un fichier d’enregistrement de décision écrit par oloproof record export, relatif à la racine du projet.

assumptions désigne ce que l’objectif tient pour acquis. Un defeater est une raison pour laquelle l’objectif pourrait être faux ; il reste ouvert jusqu’à ce que chaque élément de preuve de son resolved_by apporte un soutien. reassess_when dit ce qui devrait ramener l’équipe à l’objectif.

Le vérifier

oloproof assurance check

La vérification refuse un argumentaire qui nomme une règle absente de la politique ou un danger absent du registre, ou dont l’objectif de premier niveau ne déclare aucun périmètre, et se termine avec 2. Sinon elle affiche l’arbre, chaque objectif avec l’un de quatre statuts :

• supported : chaque élément de sa preuve et chaque sous-objectif le soutiennent, sur des preuves actuelles, et aucun contre-argument n’est ouvert ;
• undermined : une preuve échoue, est périmée ou est contredite, un sous-objectif est affaibli, ou un contre-argument est ouvert ;
• assumptions_only : rien ne le soutient, et il repose sur des hypothèses déclarées ;
• unsupported : tout le reste, chaque lacune étant nommée. Un objectif qui a un soutien et une lacune est non soutenu : une affirmation n’est pas plus solide que le point le plus faible sur lequel elle repose.

Une règle soutient un objectif quand chaque dernière exécution qui l’a décidée dit PASS, et l’affaiblit quand l’une d’elles dit FAIL ; INSUFFICIENT_EVIDENCE et MANUAL_REVIEW ne soutiennent rien. Un danger soutient quand chaque règle qui le mesure réussit. Un résultat formel soutient quand la propriété a été PROVED, et affaiblit quand elle a été DISPROVED ou quand deux résultats pour un même modèle divergent ; un résultat dit ce qu’il prouve sur le modèle formalisé, jamais sur le déploiement. Un enregistrement soutient quand son contenu a toujours pour empreinte son identifiant et que sa décision est PASS. Une preuve issue d’une exécution qui ne correspond plus au projet (son système, sa suite, ses évaluateurs ou sa politique ont changé) est périmée et affaiblit. Ces statuts sont ceux de l’argumentaire, jamais des décisions, et ils ne changent jamais un code de sortie. --json écrit le même rapport pour un pipeline.

Où il apparaît

oloproof run enregistre l’argumentaire avec l’exécution, oloproof push porte l’argumentaire de l’exécution jusqu’à votre espace de travail avec les résultats formels que nomment ses liens de preuve, et oloproof export écrit à côté des bundles la lecture qu’en fait le moteur. La page Safety and risk montre l’arbre avec chaque statut tel que le moteur l’a écrit, chaque règle liée à sa preuve. Dans l’espace de travail, l’argumentaire est lu au regard des exécutions que vous avez envoyées : la fraîcheur n’y est pas comparée, faute de fichier de projet avec lequel comparer, et les liens vers des enregistrements ne sont lus que par oloproof assurance check. Un enregistrement de décision nomme l’argumentaire que son exécution a enregistré ; record verify le présente comme la parole de l’équipe.

Pour aller plus loin

• Registre des dangers couvre les dangers sur lesquels un objectif peut reposer.
• Graphe de preuves dessine chaque affirmation avec les preuves qui la fondent.