Brontekst bekijken van Taxonomy/1. Quality/03. Formal Methods

<noinclude>{{Taxonomy/Contents}}</noinclude>
{{Taxonomy/Intro|After our general considerations about [[../1. Rationality|establishing something beyond reasonable doubt]] and about the use of [[../2. Models]] we now narrow our focus to things ''made'' for a certain goal. That brings us into the realm of engineering and, in particular, computer science.}}

[[image:Adequacy.gif|thumb|400px|left|Making a thing in order to establish properties]]Engineering is concerned with '''rational development and analysis of artefacts'''. This intention can be explained by menas of a specific version of the [[../1. Rationality|Rationality Square]], which says: An artefact is adequate when has the right structure, i.e. when it consists of the right parts, assembled in the right way. The goal of a rational approach is to keep the red arrows in the diagram as short as possible and to bridge most of the conceptual distance between structure and properties by means of forma reasoning. And the structure we invent has two purposes: not only to explain how a thing works but also to prescribe how to ''make'' it.

By '''{{*|artefact}}''' we thus mean an object in physical reality that has been or shall be intentionally constructed from certain parts for some well-defined purpose, viz. to have certain properties. This concept covers computer programs as well as complete factories, air crafts, and financial networks, but also things like bridges and hammers. 
{{Classification|Corner stones of rational development|
*properties
*specification
*blueprint
*artefact}}

Computer Science studies "dynamic" properties like the functionality (i.e. input-output relation) of {{*|program}}s or the {{*|behaviour}} of {{*|embedded system}}s. The question "which properties does it have?" often means "what does it do?" When we want to be sure that an artefact that contains and executes computer programs will ''always'' have the right behaviour, we cannot do without a completely formal, computer supported approach. Behaviour of computers is just too complex to be understood by insight or to be captured in an elegant had-written correctness proof of a few pages.

== The Rationality Square of Engineering == 
In this version of the [[../1. Rationality|Rationality Square]] the names of the corner stones and the questions between them reflect the intention of rational development:

{|  style="border:1px solid" width="75%" align="center"
| style="background:#DDDDDD" witdh="33%"|  '''{{*|blueprint}}''': a description of a structure which can be realised by assembling physical parts
| witdh="33%" |''Does every realisation of this structure have the stated properties?''
| style="background:#DDDDDD"  witdh="33%"| '''{{*|specification}}''': a description of all relevant properties
|-
| ''Does the artefact have the described structure?''
| ''Does the artefact have the properties stated by the specification?''
| ''Are the right properties stated?''
|-
|  style="background:#FFFF99" | '''{{*|artefact}}''' (an object on physical reality)
| ''Does the artefact have the desired properties?''
|  style="background:#FFFF99" | '''properties''' (in physical reality)
|}

Note that when an artefact is treated under different {{*|view}}s, we get several instances of the Rationality Square, all with the same artefact in the bottom left, but with different abstructions and different hierarchical structure. For all instances the relations between the corner stones have to be established carefully.

{{*|Computer Science}} and engineering disciplines study how this can be done generally and carefully define the relations between the corner stones in such a way that the diagram commutes. This leads to a taxonomy of research questions.

In our quest we first investigate these relations and then the corner stones, always with dynamic properties (behaviour) in mind.

== Canonical relations ==

=== Adequacy: the relation {{Taxonomy/F|has}} ===
An {{*|artefact}} {{Taxonomy/F|has}} (or has not) the desired properties. In case of dynamic properties: '''does''' (or does not) what should do. This is a relation in physical reality, established by the laws of nature. With the methods of natural science one must find mathematical spaces {{Taxonomy/F|Art}} and {{Taxonomy/F|Prop}} in which the structure of the artefacts and the properties of interest can be modelled. Then, one must define a relation {{Taxonomy/F|sat}} between these spaces such that A {{Taxonomy/F|sat}} P if and only if the artefact of which A is a model really has the properties of which P is a model.

The other relations between the corner stones have to be defined such that the diagram commutes. This gives rise to fundamental research questions.

===  Meaning: the relation {{Taxonomy/F|states}} ===
A {{*|specification}} {{Taxonomy/F|states}} certain properties. This is a matter of abstraction and a question of the semantics of the {{*|Specification language|specification language}} used. Each application area or culture may prefer their own specification language {{Taxonomy/F|Spec}} that allows to state desired properties in such a way that one can see what a specification means. This means that a relation {{Taxonomy/F|states}} has to be defined such that if the user intends a property of which P is a model, she should be able to find a formula S in {{Taxonomy/F|Spec}} such that S {{Taxonomy/F|states}} P and only P and that, ideally, it is intuitive what S states.

=== Acceptance: the relation {{Taxonomy/F|implem}} ===
Now a relation can be defined upon the previous ones: An {{*|artefact}} is an {{Taxonomy/F|implem}}entation of a {{*|specification}} if it {{Taxonomy/F|has}} the properties '''stated''' by it. 

 {{Taxonomy/DEF}} {{Taxonomy/F|implem}} := &lambda;A:{{Taxonomy/F|Art}}. &lambda;S:{{Taxonomy/F|Spec}}. &forall;P:{{Taxonomy/F|Prop}}. S {{Taxonomy/F|states}} P &rArr; A {{Taxonomy/F|has}} P 

In the absence of blueprints one often tries to ensure this by indurcive methods (tests).

=== Structure: the relation {{Taxonomy/F|real}} ===
An artefact is a {{Taxonomy/F|real}}isation of a {{*|blueprint}} if the structure defined by the blueprint is a model of the artefact. This is a question of the semantics of the {{*|blueprint language}} used. Like with specification languages, every aplication domain and culture may prefer their own blueprint language {{Taxonomy/F|Struct}}.

=== [[../4. Correctness Theorems|Correctness]]: the relation {{Taxonomy/F|sat}} ===
This is a formal relation between texts in the languages {{Taxonomy/F|Struct}} and {{Taxonomy/F|Spec}}, which can be defined upon the previous ones: A {{*|blueprint}} {{Taxonomy/F|sat}}isfies a {{*|specification}} if and only if ''all''  of its {{Taxonomy/F|real}}isations are {{Taxonomy/F|implem}}entations of that specification.

 {{Taxonomy/DEF}} {{Taxonomy/F|sat}} := &lambda;B:{{Taxonomy/F|Struct}}. &lambda;S:{{Taxonomy/F|Spec}}. &forall;A:{{Taxonomy/F|Art}}. A {{Taxonomy/F|real}} B &rArr; A {{Taxonomy/F|impl}} S 

== Corner stones ==

=== Artefacts ===
{{Classification|Our playing field|
*organisations in which IT plays a rôle
*plants or vehicles that are controlled by computers
*computer programs
*computers}}
To become a plumber you have to learn different things than to become an electrician. Different kinds of artefacts have brought forward different disciplines, each with its own education, which depends more on the materials used than on the goals. For a wooden garden fence I need a carpenter, for a metal one a smith, even if the desired properties in both cases are: keep neighbours' dogs and children out.

All these engineering disciplines have in common that they study how artefacts can be made from certain standard components, bound together in a standard way. Those standard components are understood very well, and the standard ways of construction ensure that the properties of the artefact can relativly easily be concluded from its structure. Only in rare cases some components have to be developed completely new.

Any part of an artefact can be considered as an artefact by itself, whose construction might envolve the same or a different discipline. Likewise, each artefact can be considered as a part of an enclosing artefact. Therefore, it is always essential to make the focus of attention explicit: are we reasoning about a control program inside the computer controlling a given chemical plant or are we reasoning about the purpose of the whole plant, which consists of many parts, the control program being one of them? These two focuses of attention lead to two instances of the Rationality Square.

In the sequel we will focus on artefacts wherein computer programs play an essential rôle, either as the part of a bigger artefact (e.g. a plant to be controlled), as the artefact under discussion (program construction and correctness), or because their constituting parts and execution mechanism are studied (machine architecture).

=== Properties ===
By '''{{*|property}} of an artefact''' we mean a possibly very complex, possibly dynamic physical phenomenon or set of phenomena that take place if the artefact exists. To reason formally about such properties we must define a mathematical structure to model what is relevant and to abstract from anything else. This may depend on the application domain. A special case, essential for the artefacts we are interested in, is '''observable behaviour'''. 

During the last decades many theories, languages and tools for specification and verification of behaviour have been developed, and their underlaying mathematical structure is not always evident, but usually the properties they can handle are special cases of sets of sets of atomic observations, together with some axioms.

{{Classification|Properties of dynamic systems|
* atomic observation
** what?
** where?
** when?
* scenario: a set of atomic observations
* behaviour: set of scenarios}} Why sets of sets of observations?

The abstract model must be firmly and reliably linked to physical reality. A good way to do this is to identify a set (or data type) of '''atomic observations''', each of which corresponds to a measurement in the pyisical world. Often, these atomic observations are triples (what?, where?, when?), i.e. elements of the Cartesian product of some set of '''values''', some set of '''observation points''', and some model of '''time'''. When we watch an artefact during some time at the interface with its environment, we can observe many of these triples. All of them together form a set which we may call '''{{*|scenario}}''' (and which you may call "trace", "run", or "execution", if you like). The '''{{*|behaviour}}''' of an artefact then is the set of all such scenarios it makes possible.

Although scenaros basically are sets of triples (what?, where?, when?) it can be convenient to organise them as functions from time and place (when?, where?) to values (what?) as in signal theory. If the exact moments are not of interest, they can also be organised as functions from place (where?) to sequences (what, in which order?).

Many interesting properties can be expressed in terms of such behaviour. Often, two classes can be distinguished:
; safety : some combinations of atomic observations may never occur in any scenario
; liveness : some combinations of atomic observations must occur eventually in any scenario
=== Specifications ===
A '''{{*|specification}}''' is–to be preciese– a formal description of a mathematical model of the relevant properties of an artefact to be constructed or to be investigated. When the artefact is treated under different views, each view may have its own specification. Although the text of the specification has some structure, this is not intended to imply a structure of its implementation.

When behaviour is of interest, a specification is a formula saying which scenarios are admitted and which not. 
=== Blueprints ===
A {{*|blueprint}} defines a {{*|structure}} such that an artefact can be ''made'' by realising this structure. To this end it must identify all the components of the artefact and define how they are to be bound together. A good blueprint is a formal definition of an '''<sup>7</sup>X-model''' as introduced in [[../2. Models]], in other words: the contents of a Chinese Box.

The way of binding (composition) of the physical parts depends on the kind of artefact. Resistors and drains are solderd, programming constracts are nested textually, neworks are plugged. In any case: components that are connected share something. If we are interested in behaviour, they share certain events, usually all events at a certain location, the "interface". A blueprint contains some notation that defines shared phenomena between components. For an aretefact of n components, this will be some formula with n placeholders; let us call it <sup>n</sup>X.

The components can be identified in three ways:
# By giving their respective blueprints (i.e. see them as glass boxes). Think of a circuit diagram in which the elements are small circuits themselves. This does not lead to a reduction of complexity as no extra knowlegde is included. We will not consider this possibility further.
# By giving their specifications (i.e. see them as black boxes – the {{*|Chinese Box principle}}). If the specification is simpler than their structure, this can reduce complexity considerably.
# If everything is constructed from a fixed set of elements of well-known properties (like the 118 elements of Chemistry), a pointer to a table that lists these elements is sufficient. Of course, this is equivalent to giving their specifications.

Formally, a blueprint of arity n, n>=0 is a pair (s, <sup>n</sup>X) where s is a sequence of n specifications  and <sup>n</sup>X is a structure description containing n numbered ‘place holders’ for components. <sup>n</sup>X cares for identification and renaming. If the specifications s<sub>1</sub>, s<sub>2</sub>, ... are written in terms of shared phenomena, the information how the components are boud together is already in their specifications, and <sup>n</sup>X is trivial. This is the case when we use logic as specification language, as in the explanation of the [[../4. Correctness Theorem]].


<big>Assembly: the relation {{Taxonomy/F|ass}}</big>


An artefact is or is not {{Taxonomy/F|ass}}embled (bound together) from certain components .in a cdertain way.  We write
 (a<sub>1</sub>, ... , a<sub>n</sub>) {{Taxonomy/F|ass}} <sup>n</sup>X
to denote that components (a<sub>1</sub>, ... , a<sub>n</sub>) are assembled conform the structure description <sup>n</sup>X. Now, the relation {{Taxonomy/F|real}} can be defined upon the relations {{Taxonomy/F|ass}} and {{Taxonomy/F|implem}}:
 {{Taxonomy/DEF}} {{Taxonomy/F|real}} := &lambda;A:{{Taxonomy/F|Art}}. &lambda;(s, <sup>n</sup>X):{{Taxonomy/F|Struct}}. &exist;a:{{Taxonomy/F|Art}}<sup>n</sup>. &forall;i:(1...n). a<sub>i</sub> {{Taxonomy/F|implem}} s<sub>i</sub> &and; A = a {{Taxonomy/F|ass}} <sup>n</sup>X

== Languages ==
=== Specification languages ===
To avoid the ambiguities of natural language, specifications can be accompanied by more or less formal diagrams and be written in a semi-formal or, in the hardest case, a formal language with well-defined semantics. A formal specification unambiguously defines a set of mathematical objects modelling which systems are acceptable. 

Specifications, like all contracts, necessarily are abstractions. Irrelevant details ought not to be mentioned and definitely not be formalised, but the customer should be aware not to abstract from any relevant aspect.
Many formal specification languages have been defined, each having its own advantages. It is illuminating to understand that each formal specification, in what formal language ever, is equivalent to a logical formula stating the required system properties (cf. LAMPORT, 1997). An artefact fulfils a specification if and only if that formula holds for that system. 

From this puristic viewpoint, specification languages, even if they do not resemble predicate logic notation at all, can be seen as improved notations for some carefully chosen subset of predicate logic, possibly enriched by structuring facilities. 

Specification languages must be understood by people interested in the properties of the artefact, that is customers and users. A good specification language will therefore be {{*|declarative}} and support notations familiar to the {{*|problem domain}}.

Many languages have been invented in order to allow implicit treatment  of certain aspects, to provide a compact notation supporting useful algebraic transformations, or to ensure consistency, decidability, or executability of specifications. Such language support, although being highly desirable in daily practice, can obscure the understanding of essential aspects. Authors of specification languages should be so helpful as to clarify explicitly how and why their languages differ from standard logic. If there are good reasons to have a special purpose language, users should be given a chance to understand them. Throughout this taxonomy we will frequently abstract from all such differences between specification languages. We invite the reader to share the puristic view for a while: regard each specification as a logical formula and be aware that such a formula, if completely written out, explicitly states information that may be hidden by many specification languages.

In unrestricted logic it is easy to write specifications which can never be implemented because they are logically inconsistent due to requirements that contradict each other. In a completely formal development process this will always be found out and corrected sooner or later. 

=== Blueprint languages ===
For blueprint languages the considerations are similar, only shopuld they support notations familiar to the {{*|solution domain}}.

=== Proof languages ===

Between {{*|specification}}s and {{*|blueprint}}s, the {{*|correctness}} relation '''satisfies''' must be established carefully. A proof that a {{*|blueprint}} satisfies a specification must also be written down in some suitable {{*|proof language}}. 

Computer Science is goes further than most engineering desciplines and natural science by striving for {{*|Specification language|specificationlanguages}}, {{*|blueprint language}}s, and {{*|proof language}}s that are completely {{*|formal}} and can be processed by computerised {{*|tool}}s. To this end, the [[../4. Correctness Theorems|correctness]] relation '''satisfies''' has to be defined ''syntactically''.

=== Multiple purpose languages ===

Computer science has also brought forward many languages that reside somewhere between an ideal specification language and a low-level blueprint language, in order to support various phases during [[../7. Development]].