Brontekst bekijken van Taxonomy/1. Quality/04. Correctness Theorems

<noinclude>{{Taxonomy/Contents}}</noinclude>
{{Taxonomy/Intro|The rôle of mathematics in this question can be understood in a systematic: Each correct design corresponds to a mathematical theorem. A good understanding the form and the meaning of such "correctness theorems" helps to separate issues, to focus problems, and to apply theory and tools where possible.}}
[[image:BridgingTheGap.gif|thumb|left|Bridging the gap between structure and properties by means of [[../1. Rationality|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 {{*|adequacy|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 {{*|property|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 [[../1. Rationality|Rationality Square]], assuming that all specifications are written in standard logic. In the articles on [[../7. Development]] and [[../7. Development|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".)

{{Confusion|
*[[Taxonomy/supplement/System engineering argument|System engineering argument]]}}
== Correctness ==
{{Classification|Correctness argument|
*specification of desired properties
*blueprint of artefact
**list of parts
**definition how the parts are bound together
*domain knowledge
*correctness proof}}
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<sub>1</sub>, ... , s<sub>n</sub>), <sup>n</sup>X) and a proof p for: 
 ((s<sub>1</sub>, ... , s<sub>n</sub>), <sup>n</sup>X) {{Taxonomy/F|sat}} S
With the definitions from [[../3. Formal Methods]] filled in, this comes down to proving:

 &forall;a:{{Taxonomy/F|Art}}<sup>n</sup>. &forall;i:(1...n). a<sub>i</sub> {{Taxonomy/F|implem}} s<sub>i</sub> &rArr; (a {{Taxonomy/F|ass}} <sup>n</sup>X) {{Taxonomy/F|implem}} S

or, semi-formally:

 a<sub>1</sub> {{Taxonomy/F|implem}} s<sub>1</sub> &and; a<sub>2</sub> {{Taxonomy/F|implem}} s<sub>2</sub> &and; ... &and; a<sub>n</sub> {{Taxonomy/F|implem}} s<sub>n</sub> &rArr; ((a<sub>1</sub>, ... , a<sub>n</sub>) {{Taxonomy/F|ass}} <sup>n</sup>X) {{Taxonomy/F|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 {{*|blueprint}}s, 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:
 s<sub>1</sub>&and;s<sub>2</sub>&and; ... &and;s<sub>n</sub> &rArr; S
or
 (&forall;i:(1...n). s<sub>i</sub>) &rArr; S

This is because  the parts' specifications s<sub>i</sub> 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 {{Taxonomy/F|N}} - have to be specified explicitly. If, for example, the specification s<sub>i</sub> of some part only holds in an environment where {{Taxonomy/F|N}} holds, we would have to specify:
 {{Taxonomy/F|N}}&rArr;s<sub>i</sub>

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:
 {{Taxonomy/F|N}}&and;(&forall;i:(1...n). s<sub>i</sub>) &rArr; S
where the s<sub>i</sub> are the specifications of the constituent parts of the artefact and {{Taxonomy/F|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&rArr;C. Then the theorem has the form:
 {{Taxonomy/F|N}}&and;(&forall;i:(1...n). a<sub>i</sub>&rArr;c<sub>i</sub>) &rArr; (A&rArr;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:

[[Image:Correctness_theorem.gif|400px]]

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:

 &forall;t. 
   (0 &le; t mod 5 &and; t mod 5 &lt; 3 &rArr; red(t) &and; &not; green(t))
   &and;
   (3 &le; t mod 5 &and; t mod 5 &lt; 5 &rArr; green(t) &and; &not; 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 [[../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:

 &forall;t. 
   (0 &le; t mod 5 &and; t mod 5 &lt; 3 &rArr; high(t))
   &and;
   (3 &le; t mod 5 &and; t mod 5 &lt; 5 &rArr; &not; 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:

 &forall;t. 
   (high(t) &rArr; power1(t) &and; &not; power2(t))
   &and;
   (&not; high(t) &rArr; &not; power1(t) &and; power2(t))

We assume that the bulbs never fail:

 &forall;t. power1(t)&hArr;lit1(t)

 &forall;t. power2(t)&hArr;lit2(t)

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

 &forall;t. lit1(t)&hArr;red(t)

 &forall;t. lit2(t)&hArr;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:

 (&forall;t. (0 &le; t mod 5 &and; t mod 5 &lt; 3 &rArr; high(t))&and;(3 &le; t mod 5 &and; t mod 5 &lt; 5 &rArr; &not;high(t)))
 &and;(&forall;t. (high(t) &rArr; power1(t) &and; &not;power2(t))&and;(&not; high(t) &rArr; &not;power1(t) &and; power2(t)))
 &and;(&forall;t. power1(t) &hArr; lit1(t))
 &and;(&forall;t. power2(t) &hArr; lit2(t))
 &and;(&forall;t. lit1(t) &hArr; red(t))
 &and;(&forall;t. lit2(t) &hArr; green(t))
 &rArr;
 (&forall;t. (0 &le; t mod 5 &and; t mod 5 &lt; 3 &rArr; red(t)&and;&not;green(t))&and;(3 &le; t mod 5 &and; t mod 5 &lt; 5 &rArr; green(t)&and;&not;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&le;n. So we arrive at a generic correctness theorem:

 &forall;m, n. m&le;n &rArr;
 (&forall;t. (0 &le; t mod n &and; t mod n &lt; m &rArr; high(t))&and;(m &le; t mod n &and; t mod n &lt; n &rArr; &not;high(t)))
 &and;(&forall;t. (high(t) &rArr; power1(t) &and; &not;power2(t))&and;(&not; high(t) &rArr; &not;power1(t) &and; power2(t)))
 &and;(&forall;t. power1(t) &hArr; lit1(t))
 &and;(&forall;t. power2(t) &hArr; lit2(t))
 &and;(&forall;t. lit1(t) &hArr; red(t))
 &and;(&forall;t. lit2(t) &hArr; green(t))
 &rArr;
 (&forall;t. (0 &le; t mod n &and; t mod n &lt; m &rArr; red(t)&and;&not;green(t))&and;(m &le; t mod n &and; t mod n &lt; n &rArr; green(t)&and;&not;red(t))

=== The same in {{*|Uppaal}} ===
{{!|Hanno Wupper||Zou iemand dit naar {{*|Uppaal}} kunnjen vertalen? Bij voorbaat bedankt!}}

=== 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
==== Predicate logic ====
==== Modal logic ====
==== Automata ====
==== 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(.....