A.20:4.2 - Applicability, required set, and summary

Before evaluation, name the constraints applicable to the current subject and case. Mark each as required, optional, or notApplicable and state why. The required set is complete only when every constraint that the current use depends on is named.

For one evaluated applicable constraint:

• satisfied means the test established the named constraint for the stated case and window;
• violated means the test established a counterexample or failed condition;
• unknown means required facts, applicability facts, or witness content could not be determined;
• error means the selected evaluation could not complete correctly.

When a consumer needs one local summary over the complete required set, use:

ConstraintValiditySummary ∈ {satisfied, violated, unresolved, notApplicable}.

The summary rule is:

1. notApplicable only when the declared required set is empty because no A.20 internal constraint applies to this subject and use;
2. violated when at least one required result is violated;
3. unresolved when no required result is violated but at least one required constraint is notRun, unknown, or error; and
4. satisfied only when every required applicable constraint has an evaluated satisfied result.

Optional results do not change the summary unless a separately accepted use decision moves their constraints into the required set. A missing required result can therefore never disappear beside a satisfied result.