Güvence argümanları

Güvence argümanı, ekibinizin bir sistemin belirtilen bir kullanım için yeterince iyi olduğuna dair savıdır: her iddia, hangi kullanım için yapıldığı ve dayandığı kanıt. Argüman, sürüm politikasının yanında assurance.yaml içinde durur; böylece pull request'lerde incelenir ve Oloproof her iddiayı elindeki kanıta karşı okur. Bir iddianın kanıtlandığını asla söylemez: hangi iddiaların güncel ve geçen kanıta, hangilerinin geçmeyen, eskimiş ya da eksik kanıta, hangilerinin yalnızca varsayımlara dayandığını söyler.

Argümanı yazmak

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]

Bir hedef bir iddiadır. En üst düzeydeki bir hedef scope değerini, yani iddianın yapıldığı amaçlanan kullanımı belirtir; alt hedef bunu devralır. strategy, alt hedeflerin hedefi nasıl desteklediğini sözcüklerle anlatır. Her evidence öğesi aşağıdakilerden tam olarak birini adlandırır:

• rule: release.yaml içindeki bir kural; her sistemin her süitteki son çalıştırmasında okunur; system ve suite hangi çalıştırmaların sayılacağını daraltır;
• hazard: hazards.yaml içindeki bir tehlike (Tehlike kaydı);
• proof: bir ispat kuralının okuduğu gibi okunan biçimsel bir özellik (Biçimsel ispatlar): özellik için alınan son sonuç, aynı modelin bir DISPROVED sonucu üstün gelir; model (bir özet) onu tek bir biçimselleştirilmiş modelle sınırlar; proje bir sonuca sahip olana dek bağlantı hiçbir şeyi desteklemez;
• record: oloproof record export tarafından yazılmış, proje köküne göre yolu verilen bir karar kaydı dosyası.

assumptions, hedefin doğru kabul ettiği şeylerdir. Bir defeater, hedefin yanlış olabileceğine dair bir nedendir; resolved_by içindeki kanıtın her öğesi onu destekleyene dek açık kalır. reassess_when, ekibi hedefe neyin geri döndürmesi gerektiğini söyler.

Kontrol etmek

oloproof assurance check

Kontrol, politikada olmayan bir kuralı ya da kayıtta olmayan bir tehlikeyi adlandıran veya en üst düzey hedefi kapsam belirtmeyen bir argümanı reddeder ve 2 ile çıkar. Aksi halde ağacı yazdırır; her hedef dört durumdan biriyle gösterilir:

• supported: kanıtının her öğesi ve her alt hedefi onu güncel kanıtla destekler ve hiçbir itiraz açık değildir;
• undermined: kanıtın bir kısmı geçmez, eskimiştir ya da çelişkilidir, bir alt hedef zayıflatılmıştır veya bir itiraz açıktır;
• assumptions_only: hiçbir şey onu desteklemez ve belirtilen varsayımlara dayanır;
• unsupported: geri kalan her durum; her boşluk adlandırılır. Bir miktar desteği ve bir boşluğu olan hedef desteklenmemiştir: bir iddia, dayandığı en zayıf şey kadar güçlüdür.

Bir kural, onu karara bağlayan her son çalıştırma PASS dediğinde hedefi destekler, herhangi biri FAIL dediğinde zayıflatır; INSUFFICIENT_EVIDENCE ve MANUAL_REVIEW hiçbir şeyi desteklemez. Bir tehlike, onu ölçen her kural geçtiğinde destekler. Biçimsel bir sonuç, özellik PROVED olduğunda destekler; DISPROVED olduğunda ya da aynı model için iki sonuç çeliştiğinde zayıflatır; bir sonuç, biçimselleştirilmiş model hakkında neyi kanıtladığını söyler, asla dağıtım hakkında değil. Bir kayıt, içeriğinin özeti hâlâ kimliğine eşitse ve kararı PASS ise destekler. Artık projeyle eşleşmeyen (sistemi, süiti, değerlendiricileri ya da politikası değişmiş) bir çalıştırmadan gelen kanıt eskimiştir ve zayıflatır. Bu durumlar argümana aittir, asla karar değildir ve bir çıkış kodunu asla değiştirmez. --json aynı raporu bir işlem hattı için yazar.

Nerede görünür

oloproof run argümanı çalıştırmayla birlikte kaydeder, oloproof push çalıştırmanın argümanını, ispat bağlantılarının adlandırdığı biçimsel sonuçlarla birlikte çalışma alanınıza taşır ve oloproof export motorun onu okuyuşunu paketlerin yanına yazar. Safety and risk sayfası ağacı, her durumu motorun yazdığı haliyle gösterir; her kural kanıtına bağlanır. Çalışma alanında argüman, gönderdiğiniz çalıştırmalara karşı okunur: orada güncellik karşılaştırılmaz, çünkü karşılaştırılacak bir proje dosyası yoktur, ve kayıt bağlantılarını yalnızca oloproof assurance check okur. Bir karar kaydı, çalıştırmasının kaydettiği argümanı adlandırır; record verify onu ekibin sözü olarak bildirir.

Sonraki adımlar

• Tehlike kaydı, bir hedefin dayanabileceği tehlikeleri anlatır.
• Kanıt grafiği, her iddiayı altındaki kanıtla birlikte çizer.