Practical guide
Make combinations of rules visible with a decision table
Rules become hard to review when each one lives in a separate sentence. A decision table puts input combinations and their expected outcomes in one place.
Start with a decision someone must make
Choose a specific question, such as whether an account may export a document. Identify the inputs that change the answer, give each a finite domain and name the output precisely. A general decision table also needs an explicit policy for overlapping rows. The OMG Decision Model and Notation specification formalizes these concepts; a table in Proof uses its own supported data model.
Illustrative table: an export policy
| Role | Published? | Export allowed? |
|---|---|---|
| Owner | No | Yes |
| Owner | Yes | Yes |
| Reader | No | No |
| Reader | Yes | Yes |
These four cells cover the two declared roles and publication states. Adding a support role without its outcomes leaves missing cells. Adding a second Owner/No cell with a different outcome creates a conflict. A default can fill holes, but “default deny” is itself a product decision. Review it rather than assuming every omitted case should inherit it.
Check the authored table in Proof
Proof's current table model uses concrete enum and boolean cells in domain.tables in a component variable file. Author the YAML, validate it and inspect its grid. Completeness covers cells or an explicit default. Consistency comes from duplicate-cell validation, not a separate SMT theorem. Supported equivalent_to links can compare corresponding outputs.
proof validate
proof var table show export export_permissions
proof check tables specs/system export
These component and table names are examples. The table command is read-only; it does not invent policy or derive it from code.
Make each important cell observable
For Reader/No, call the real export entry point and assert rejection and absence of an exported artifact. For an allowed cell, assert the expected artifact, not just a successful return. Retain the executed result and revision. A complete table says that the declared combinations have outcomes; it does not show the roles are exhaustive, the policy is correct or the implementation follows it.
Keep changes reviewable
Review changed cells with the requirement amendment. A new role or state should prompt a fresh completeness check and targeted tests. Record why the new output is acceptable so later edits preserve the decision, rather than merely retaining a grid that still looks complete.
Follow the evidence
Sketch a table for one disputed decision, then bring the policy and its implementation to a review.