cli.Checked

One application of a contracted transform in the file, and its proof.

Usage

Source

cli.Checked(
    name,
    nodes,
    report,
    links,
    params,
    transform,
)

Attributes

name: str

The transform’s name.

nodes: list[str]

The file’s variables that hold the node this application built (empty when no variable does, or it built an Ibis table).

report: Report | None

The sverify.Report of its postconditions; None when the budget ran out before it was proved.

links: list[str]

Why a precondition on another transform’s result does not follow from that transform’s guarantees, one message each.

params: dict[str, str]

For each input table the report names, the parameter of the transform that reads it.

transform: ContractedTransform

The sverify.ContractedTransform.

Attributes

Name	Description
status	"proved"; "checked", when every postcondition it does not

---

status

"proved"; "checked", when every postcondition it does not

status: Status

prove is checked on the data at each refresh (on_unproved="check") and nothing else is missing; "not_proved"; or "unfinished", when the budget ran out first.