Langsung ke konten
Dokumentasi
Log perubahanHargaBuka konsol

Panduan

Graf bukti

Graf bukti adalah segala hal yang menjadi dasar sebuah keputusan rilis, ditulis sebagai node bertipe dan edge bertipe dalam satu berkas JSON. Graf ini memuat versi sistem, suite, dan evaluator yang dievaluasi sebuah run, estimasi yang dihitung darinya, keputusan yang membacanya di bawah sebuah kebijakan, persetujuan yang mengesahkannya, bahaya yang diukurnya, klaim kasus jaminan yang didukungnya, dan hasil formal di sampingnya. Graf ini juga menyebut di mana bukti tidak lengkap, usang, atau bertentangan, sehingga peninjau melihat celahnya sebelum membaca hal lain.

Menggambarnya

oloproof evidence graph --out graph.json
oloproof evidence graph run_01J9 --out run.json
oloproof evidence graph --record decision-record.json --out record-graph.json

Tanpa run, graf mencakup run terakhir setiap sistem di setiap suite, run yang sama yang dipakai untuk membaca daftar bahaya dan kasus jaminan. Dengan id run, graf mencakup run itu dan setiap klaim yang membacanya. Dengan --record, graf digambar dari berkas rekaman keputusan saja, sehingga pihak kedua dapat melihat apa yang dibawa rekaman itu tanpa store Anda; apa yang hanya disebut oleh rekaman (daftar bahaya dan kasus jaminannya, berdasarkan digest) dicantumkan dalam catatan. Tanpa --out graf dicetak.

Isinya

Berkas itu menyatakan "graph": "oloproof.evidence_graph/v1". Setiap node memiliki id (bertipe, misalnya run:run_01J9 atau decision:run_01J9/label-floor), type, label, attributes (status, interval, digest), dan basis, yaitu apa yang menjadi dasarnya:

  • computed oleh mesin dari bukti yang tercatat: estimasi dengan intervalnya, sebuah keputusan;
  • signed oleh runner terdaftar, yang tanda tangannya diperiksa oloproof record verify;
  • attested oleh orang yang disebut namanya: kebijakan rilis, persetujuan, bahaya, klaim;
  • imported dari alat lain: skor yang dibaca oloproof scores import, hasil sebuah solver.

Tipe node-nya adalah system_version, suite_version, evaluator_version, run, estimate, decision, policy, signoff, hazard, claim, dan proof. Edge juga bertipe: sebuah run evaluates versi sistem dan berjalan on_suite pada versi suite; estimasi bersifat computed_from sebuah run dan judged_by versi evaluator; keputusan reads estimasi under_policy sebuah kebijakan; persetujuan approves keputusan; bahaya bersifat measured_by keputusan; dan klaim bersifat supported_by keputusan, bahaya, hasil formal, dan sub-tujuannya.

Apa yang dilaporkannya

  • dangling: edge yang targetnya tidak ada di graf, beserta alasannya. Bahaya yang menyebut aturan yang tidak diputuskan sebuah run, atau keputusan yang metriknya tidak punya hasil tersimpan, muncul di sini alih-alih menghilang.
  • stale: run yang buktinya tidak lagi cocok dengan pembandingnya, beserta setiap alasan dan setiap node yang bertumpu padanya. Secara lokal, run dibandingkan dengan proyek seperti saat ini; di ruang kerja, dan tanpa berkas proyek, dengan run terbaru di store untuk sistem dan suite yang sama. Graf yang digambar dari rekaman tidak melaporkan apa pun sebagai usang, karena tidak ada pembandingnya.
  • contradictions: dua hasil formal untuk satu properti dan satu model yang saling bertentangan, dan klaim yang diargumenkan dari bukti yang gagal.

Tidak ada apa pun dalam graf yang memutuskan sesuatu: statusnya adalah keputusan mesin, dan status sebuah klaim adalah yang dilaporkan oloproof assurance check.

Di ruang kerja

Halaman bukti sebuah run menawarkan graf untuk diunduh, digambar oleh mesin dari bukti yang Anda push, di samping rekaman keputusan dari run yang tunduk pada tata kelola.

Langkah selanjutnya