Taxonomy/1. Quality/04. Correctness Theorems

Bridging the gap between structure and properties by means of rationality

"How can we be sure?" This chapter focuses the long black arrow.

The highest level of certainty is provided by a mathematical – formal – proof. We can be sure that an →artefact is →adequate if we can prove a theorem that bridges the gap between a →blueprint describing the →structure of the artefact and a →specification of the desired →properties. Provided, of course, that the red arrows hold. What does such a "correctness theorem" theorem look like?

We will first investigate the form in which it emerges from the relations of the Rationality Square, assuming that all specifications are written in standard logic. In the articles on Taxonomy/1. Quality/7. Development and development as creative mathematical activity we will demonstrate how a good understanding of the essence of the correctness theorem can help in system analysis, development, and verification even if formal methods are never apllied so far that an actual theorem is ever written down. Understanding the idea can help even if a complete →formal theorem is an unreachable ideal. (See →Roel Wieringa's "System engineering argument".)

Correctness

Since specifications and blueprints are mathematical objects (descriptions of properties and structure), we can capture the essence of an information technologist’s task in mathematical terms. In order to design an artefact with certain properties he or she must produce a "Chinese Box" consisting of a specification S, a blueprint ((s₁, ... , s_n), ⁿX) and a proof p for:

((s1, ... , sn), nX) sat S

With the definitions from Taxonomy/1. Quality/3. Formal Methods filled in, this comes down to proving:

∀a:Artn. ∀i:(1...n). ai implem si ⇒ (a ass nX) implem S

or, semi-formally:

a1 implem s1 ∧ a2 implem s2 ∧ ... ∧ an implem sn ⇒ ((a1, ... , an) ass nX) implem S

This is the most general form of what we shall call a correctness theorem.

Logic as specification language

Many powerful →specification and →blueprint languages have been defined. We can observe that the more useful such a language is in practise, the more complicated its semantics and the more difficult it can be related to other languages. This is due to domain knowledge built into such languages, but also, as explained about →blueprints, due to →renaming, →identification, and →hiding.

Using plain propositional or predicate logic, without anything built in, without features for renaming or context-shift, as a specification language has advantages and disadvantages. In general, we can say that plain logic is more suitable to explain the essence of the Correctness Theorem, while more powerful languages are much more suitable to actually write one for a gtiven artefact.

The properties of an artefact are implied by the properties of its parts

The greatest advantage of predicate logic is that the form of the correctness theorem becomes very simple:

s1∧s2∧ ... ∧sn ⇒ S

or

(∀i:(1...n). si) ⇒ S

This is because the parts' specifications s_i talk about the same shared phenomena and so already contain all information about the connection of parts. If two parts share an interface, their specifications will both talk about this interface. Therefore, the X of the blueprint is trivial.

Laws of nature, environment

The greatest disadvantage is that the specifications really must state everything we need to complete the proof of the theorem, as no knowledge is built into the language. Which means that, among others, all necessary laws of nature and mathematical axioms - let us call them N - have to be specified explicitly. If, for example, the specification s_i of some part only holds in an environment where N holds, we would have to specify:

N⇒si

Instead of "coding" these laws in the specifications of all the artefact's parts, we can assume that Nature also is a part, or, of you like, the environment of the parts. The correctness theorem then becomes:

N∧(∀i:(1...n). si) ⇒ S

where the s_i are the specifications of the constituent parts of the artefact and N are the laws of nature we need to be able to complete the proof.

A realistic →specification often is an assumption-commitment pair (A, C), which in predicate logic comes down to A⇒C. Then the theorem has the form:

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

We call this the canonical form of the Correctness Theorem for artefacts.

Generalisation

For a concrete artefact this will contain quantities for durations, lengths, speeds, etc., which all have to fit with each other. Instead of proving a specific theorem, we can try to prove a more general theorem.

A generic correctness theorem, formulated in predicate logic, for an →artefact of n+1 components with respect to a desired set of properties is a true formula of the form:

where the phii, psii, PHI and PSI are variables for quantities and PI is a predicate defining for which combinations of quantities the theorem holds.

Examples

A realistic correctness theorem in predicate logic

The artefact under discussion is a traffic light for pedestrians. It consists of, among others, bulbs, stained glass, cables, switches, and a timer.

This traffic light is a part of a bigger artefact: a crossing with several similar lights and possibly sensors. At that higher level of decomposition one might want to prove that the lights and sensors together ensure the absence of accidents. The blueprint that is proved correct at that higher level might requirere a traffic light that switches between red and green at certain intervals. This is the specification we take as given at the level under discussion.

The whole crossing, and thus our light, can be analysed under different views. We choose a view that abstracts from the intensity of the red and green light, from the specific colour spectrum, the size of the lit areas, the prevention of reflection, the possibility of dirt or heavy storms etc., etc. The only question we treat at our view is that the right colours are lit at the right moments.

To specify the desired behaviour in predicate logic, two time-dependent predicates are sufficient. Each corresponds to an observation in the physical world:

red(t) 

true if and only if at moment t the physical traffic emits red light

green(t) 

true if and only if at moment t the physical traffic emits green light

We must also fix our model of time. For this problem, real numbers with unit minute are fine.

The overall specification then could be something like:

∀t. 
  (0 ≤ t mod 5 ∧ t mod 5 < 3 ⇒ red(t) ∧ ¬ green(t))
  ∧
  (3 ≤ t mod 5 ∧ t mod 5 < 5 ⇒ green(t) ∧ ¬ red(t))

The same meaning can be expressed in the same predicate logic by many different, logically equivalent formulae. In an extended predicate logic with intervals it can be expressed shorter. Even shorter, and possibly more readable, it can be expressed in process algebra. Maybe traffic light experts have a language, difficult to read for us, in which they find they can express the same much more readable. In practice one should choose a specification language and a style of writing that supports readability as good as possible, see Taxonomy/1. Quality/10. Quality criteria.

At the higher level of the surrounding crossing such a specification would occur at the left side of the correctness theorem as specification of one part. One might like to prove that this one never is green at the same time as another one. But let us stay at our level! Here, the specification will form the right hand side of the correctness theorem.

We can decompose the physical traffic light in several ways. We choose a decomposition into a timer, a switch, two bulbs, and two stained glasses. If you like, you can choose a different decomposition and, for example, consider a bulb together with its stained glass as just one constituting part.

To specify their behaviour we need predicates that correspond to measurements at their interfaces:

high(t) 

true if and only if the output port of the timer is "high"

power1(t) 

true if and only if bulb 1 is powered

power2(t) 

true if and only if bulb 2 is powered

lit1(t) 

true if and only if bulb 1 is lit

lit2(t) 

true if and only if bulb 2 is lit

The timer lets its output oscillate in a certain way:

∀t. 
  (0 ≤ t mod 5 ∧ t mod 5 < 3 ⇒ high(t))
  ∧
  (3 ≤ t mod 5 ∧ t mod 5 < 5 ⇒ ¬ high(t))

At a lower level, where we might want to prove that the timer is correctly implemented by a computer plus →software, this specification would form the right hand side of another correctness theorem.

The switch controls the electricity fot the two bulbs conforming to the output of the timer:

∀t. 
  (high(t) ⇒ power1(t) ∧ ¬ power2(t))
  ∧
  (¬ high(t) ⇒ ¬ power1(t) ∧ power2(t))

We assume that the bulbs never fail:

∀t. power1(t)⇔lit1(t)

∀t. power2(t)⇔lit2(t)

Finally, we assume that the glasses do nothing but change the colour of the light:

∀t. lit1(t)⇔red(t)

∀t. lit2(t)⇔green(t)

The reader may doubt all these assumptions. This is exactly why an explicit correctness theorem is useful: it makes all assumptions explicit. Otherwise, nothing could be proved. Anyway, with these assumptions the full correctness theorem would be:

(∀t. (0 ≤ t mod 5 ∧ t mod 5 < 3 ⇒ high(t))∧(3 ≤ t mod 5 ∧ t mod 5 < 5 ⇒ ¬high(t)))
∧(∀t. (high(t) ⇒ power1(t) ∧ ¬power2(t))∧(¬ high(t) ⇒ ¬power1(t) ∧ power2(t)))
∧(∀t. power1(t) ⇔ lit1(t))
∧(∀t. power2(t) ⇔ lit2(t))
∧(∀t. lit1(t) ⇔ red(t))
∧(∀t. lit2(t) ⇔ green(t))
⇒
(∀t. (0 ≤ t mod 5 ∧ t mod 5 < 3 ⇒ red(t)∧¬green(t))∧(3 ≤ t mod 5 ∧ t mod 5 < 5 ⇒ green(t)∧¬red(t))

The proof of this theorem does not depend on the specific numbers 3 and 5. It is easy to prove a more general theorem for variables m and n, provided m≤n. So we arrive at a generic correctness theorem:

∀m, n. m≤n ⇒
(∀t. (0 ≤ t mod n ∧ t mod n < m ⇒ high(t))∧(m ≤ t mod n ∧ t mod n < n ⇒ ¬high(t)))
∧(∀t. (high(t) ⇒ power1(t) ∧ ¬power2(t))∧(¬ high(t) ⇒ ¬power1(t) ∧ power2(t)))
∧(∀t. power1(t) ⇔ lit1(t))
∧(∀t. power2(t) ⇔ lit2(t))
∧(∀t. lit1(t) ⇔ red(t))
∧(∀t. lit2(t) ⇔ green(t))
⇒
(∀t. (0 ≤ t mod n ∧ t mod n < m ⇒ red(t)∧¬green(t))∧(m ≤ t mod n ∧ t mod n < n ⇒ green(t)∧¬red(t))

The same in →Uppaal

Zou iemand dit naar →Uppaal kunnjen vertalen? Bij voorbaat bedankt!
Hanno Wupper → Taxonomy	Remove this comment when resolved!

Small examples in different notations

As said earlier, in the daily practice of development and verification correctness theorems appear in many languages and notations. Here some simple examples.

Propositional logic

cd-example from B&B

Types

In typed lambda-calculus, the type system ensures that the correctness theorem holds:

f: A->B, g: B->C |- g f : A->C

wp (Dijkstra)

wp-calculus 

In →A Discipline of Programming, →E. W. Dijkstra teaches us how to reason about programs by means of pre- and postconditions. In his calculus, a typical correctness theorem would be:

wp(.....