가이드
보증 사례
보증 사례는 시스템이 명시된 용도에 충분히 좋다는 팀의 논증으로, 각 주장과 그 주장이 대상으로 하는 용도, 그리고 주장이 기대는 증거로 이루어집니다. 사례는 릴리스 정책 옆 assurance.yaml 에 있어 풀 리퀘스트에서 검토되며, Oloproof 는 각 주장을 보유한 증거에 비추어 읽습니다. 주장이 증명되었다고는 결코 말하지 않습니다. 어떤 주장이 현재의 통과한 증거에 기대는지, 어떤 주장이 실패했거나 오래되었거나 누락된 증거에 기대는지, 어떤 주장이 가정에만 기대는지를 말합니다.
사례 작성
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]목표는 주장입니다. 최상위 목표는 scope, 즉 그 주장이 대상으로 하는 의도된 용도를 밝히며, 하위 목표는 이를 물려받습니다. strategy 는 하위 목표가 목표를 어떻게 논증하는지를 말로 적습니다. evidence 의 각 항목은 다음 중 정확히 하나를 지명합니다.
- rule: release.yaml 의 규칙으로, 각 시스템의 각 스위트 최신 실행에서 읽습니다. system 과 suite 는 어떤 실행을 셀지 좁힙니다.
- hazard: hazards.yaml 의 위험 요소(위험 요소 등록부).
- proof: 형식적 속성으로, 증명 규칙이 읽는 방식대로 읽습니다(형식 증명). 그 속성에 대해 마지막으로 받은 결과이며, 같은 모델의 DISPROVED가 우선합니다. model(다이제스트)은 하나의 형식화된 모델로 좁힙니다. 프로젝트가 결과를 보유하기 전까지 이 연결은 아무것도 뒷받침하지 않습니다.
- record: oloproof record export 가 쓴 결정 레코드 파일로, 프로젝트 루트 기준 상대 경로입니다.
assumptions 는 목표가 당연하게 여기는 것입니다. defeater 는 목표가 거짓일 수 있는 이유이며, resolved_by 의 모든 증거가 그것을 뒷받침할 때까지 열린 상태로 남습니다. reassess_when 은 무엇이 팀을 목표로 다시 돌아가게 해야 하는지를 말합니다.
확인하기
oloproof assurance check확인은 정책에 없는 규칙이나 등록부에 없는 위험 요소를 지명하거나, 최상위 목표가 범위를 밝히지 않은 사례를 거부하고 2 로 종료합니다. 그렇지 않으면 트리를 출력하며, 각 목표에 다음 네 가지 상태 중 하나를 붙입니다.
- supported: 모든 증거 항목과 모든 하위 목표가 현재 증거로 목표를 뒷받침하고, 열린 반박 요인이 없습니다.
- undermined: 어떤 증거가 실패했거나 오래되었거나 모순되거나, 하위 목표가 약화되었거나, 반박 요인이 열려 있습니다.
- assumptions_only: 아무것도 목표를 뒷받침하지 않으며, 명시된 가정에 기댑니다.
- unsupported: 그 밖의 모든 경우로, 각 공백의 이름이 나옵니다. 일부 뒷받침과 공백이 함께 있는 목표는 뒷받침되지 않은 것입니다. 주장은 그것이 기대는 가장 약한 것만큼만 강합니다.
규칙은 그것을 결정한 모든 최신 실행이 PASS 라고 할 때 목표를 뒷받침하고, 어느 하나라도 FAIL 이라고 하면 약화합니다. INSUFFICIENT_EVIDENCE 와 MANUAL_REVIEW 는 아무것도 뒷받침하지 않습니다. 위험 요소는 그것을 측정하는 모든 규칙이 통과할 때 뒷받침합니다. 형식 검증 결과는 속성이 PROVED 일 때 뒷받침하고, DISPROVED 이거나 한 모델에 대한 두 결과가 서로 어긋날 때 약화합니다. 결과가 증명하는 것은 형식화된 모델에 관한 것이며, 결코 배포에 관한 것이 아닙니다. 레코드는 그 내용의 다이제스트가 여전히 그 ID 와 일치하고 그 결정이 PASS 일 때 뒷받침합니다. 더 이상 프로젝트와 일치하지 않는 실행(시스템, 스위트, 평가기 또는 정책이 바뀐 경우)의 증거는 오래된 것이며 약화합니다. 이 상태들은 사례의 것이지 결코 결정이 아니며, 종료 코드를 바꾸지 않습니다. --json 은 같은 보고서를 파이프라인용으로 씁니다.
표시되는 곳
oloproof run 은 실행과 함께 사례를 기록하고, oloproof push 는 실행의 사례를 그 증명 연결이 지명하는 형식 검증 결과와 함께 워크스페이스로 보내며, oloproof export 는 엔진이 사례를 읽은 결과를 번들 옆에 씁니다. Safety and risk 페이지는 엔진이 쓴 그대로의 각 상태와 함께 트리를 보여 주며, 각 규칙은 그 증거로 연결됩니다. 워크스페이스에서는 사례를 푸시한 실행에 비추어 읽습니다. 비교할 프로젝트 파일이 없으므로 그곳에서는 최신성을 비교하지 않으며, 레코드 연결은 oloproof assurance check 만 읽습니다. 결정 레코드는 그 실행이 기록한 사례를 지명하고, record verify 는 이를 팀의 말로 보고합니다.