Taxonomy/1. Quality/05. Focus

Development and verification and validation problems can be moving targets, and discussions about correctness can be confusing. Are we, for example, talking about finding a control program for a plant or about finding its specification? What do we know about its environment? Is there a blueprint, and, if yes, of what? Which specifications are given and how "hard" are they? What may be changed? What is the overall goal?

A specification of an artefact occurs at the right hand side of a correctness theorem if that artefact has still to be designed or if it already exists and has to be validated. The same specification occurs at the left hand side of a Correctness Theorem when the question is whether it is the right part in a surrounding artefact. This gives rise to a tree of correctness theorems.

To pin down a problem one should focus on the correctness theorem at one particular level and use a checklist to define what is given and what has to be found out. If, at that level, the overall specification is not given, one has to find a correctness theorem at the next higher level for the surrounding artefact, of which the artefact under discussion is a constituting part. Likewise, when the specifications of the parts of the artefact under discussion are not known, it may be a good idea to study correctness theorems at the nex lower level. In any case, a good discipline is always to state the level of focus of attention and not to swich implicitly bewteen levels.

(The principles established here will be elaborated in Taxonomy/2. Methodology/1. Problem statement, Taxonomy/3. Non-Monotonic Refinement and Taxonomy/1. Quality/7. Development.)

Unknowns

A taxonomy of verification and validation problems.

Assumptions

Formal treatment of correctness issues is always based on assumptions. A number of them will be stated explicitly, others are left implicit. When languages other than predicate logic are used, assumptions may also be built into the language.

The canonical form of the correctness theorem allows to distinguish between several classes of assumptions.

N∧(∀i:(1...n). ai⇒ci) ⇒ (A⇒C)

Implicit assumptions

The correctness theorem is meaningful in a physical reality where the component's specifications really hold, i.e. where N⇒(a_i⇒c_i) is true. Therefore one is tempted to put all knowledge about nature and mathematics into formula N. This would, however, make N infinitely large.

It is good mathematical practise not to state more knowledge in a theorem than necessary for its proof. So we put only those laws into N that are needed to prove the theorem and leave the rest implicit.

Explicit assumptions

... that are stated explicitly because they are essential for the correctness proof