Pular para o conteúdo
Docs
Registro de alteraçõesPreçosAbrir o console

Guias

Casos de garantia

Um caso de garantia é o argumento da equipe de que um sistema é bom o bastante para um uso declarado: cada afirmação, o uso a que se destina e a evidência que a apoia. O caso fica ao lado da política de lançamento, em assurance.yaml, então é revisado em pull requests, e o Oloproof lê cada afirmação contra a evidência que possui. Ele nunca diz que uma afirmação está provada: diz quais afirmações se apoiam em evidência atual que passa, quais em evidência que falha, desatualizada ou ausente, e quais apenas em premissas.

Escrevendo o 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]

Um objetivo é uma afirmação. Um objetivo de nível superior declara seu scope, o uso pretendido para o qual a afirmação é feita; um subobjetivo o herda. strategy diz em palavras como os subobjetivos sustentam o objetivo. Cada item de evidence nomeia exatamente um destes:

  • rule: uma regra do release.yaml, lida na última execução de cada sistema em cada suíte; system e suite restringem quais execuções contam;
  • hazard: um perigo do hazards.yaml (Registro de perigos);
  • proof: uma propriedade formal, lida como uma regra de prova a lê (Provas formais): o último resultado recebido para a propriedade, com um DISPROVED do mesmo modelo prevalecendo; model (um digest) a restringe a um único modelo formalizado; enquanto o projeto não possuir um resultado, o vínculo não sustenta nada;
  • record: um arquivo de registro de decisão escrito por oloproof record export, relativo à raiz do projeto.

assumptions são o que o objetivo dá como certo. Um defeater é uma razão pela qual o objetivo pode ser falso; ele continua aberto até que cada item da evidência em seu resolved_by o sustente. reassess_when diz o que deve fazer a equipe voltar ao objetivo.

Verificando

oloproof assurance check

A verificação recusa um caso que nomeia uma regra que a política não tem ou um perigo que o registro não tem, ou cujo objetivo de nível superior não declara escopo, e termina com 2. Caso contrário, imprime a árvore, cada objetivo com um de quatro status:

  • supported: cada item da sua evidência e cada subobjetivo o sustentam, com evidência atual, e nenhuma objeção está aberta;
  • undermined: alguma evidência falha, está desatualizada ou é contradita, um subobjetivo está enfraquecido, ou uma objeção está aberta;
  • assumptions_only: nada o sustenta, e ele se apoia em premissas declaradas;
  • unsupported: qualquer outro caso, com cada lacuna nomeada. Um objetivo com algum suporte e uma lacuna não está sustentado: uma afirmação é tão forte quanto a coisa mais fraca em que se apoia.

Uma regra sustenta um objetivo quando toda última execução que a decidiu diz PASS, e o enfraquece quando alguma diz FAIL; INSUFFICIENT_EVIDENCE e MANUAL_REVIEW não sustentam nada. Um perigo sustenta quando toda regra que o mede passa. Um resultado formal sustenta quando a propriedade foi PROVED, e enfraquece quando foi DISPROVED ou quando dois resultados para um mesmo modelo discordam; um resultado diz o que prova sobre o modelo formalizado, nunca sobre a implantação. Um registro sustenta quando o digest do seu conteúdo ainda é igual ao seu id e sua decisão é PASS. Evidência de uma execução que não corresponde mais ao projeto (seu sistema, suíte, avaliadores ou política mudaram) está desatualizada e enfraquece. Esses status são do caso, nunca decisões, e nunca mudam um código de saída. --json escreve o mesmo relatório para um pipeline.

Onde aparece

oloproof run registra o caso com a execução, oloproof push leva o caso da execução ao seu espaço de trabalho com os resultados formais que os seus vínculos de prova nomeiam, e oloproof export escreve a leitura que o motor faz dele ao lado dos bundles. A página Safety and risk mostra a árvore com cada status como o motor o escreveu, cada regra ligada à sua evidência. No espaço de trabalho, o caso é lido contra as execuções que você enviou com push: a atualidade não é comparada ali, porque não há arquivo de projeto com que comparar, e os vínculos para registros são lidos apenas por oloproof assurance check. Um registro de decisão nomeia o caso que a sua execução registrou; record verify o apresenta como a palavra da equipe.

Próximos passos