Taxonomy/1. Quality/06. Software

{Taxonomy/Intro|Rationality Squares and Correctness Theorems can be applied to all artefacts, whether they contain computer programs or not. This chapter places hardware and software into their context.}}

The hardware of a contemporary computer is a very complex artefact, extremely difficult to design and realise. Its specification, however, is relatively simple: a universal machine. Due to its universality one often abstracts from its existence altogether. This can make reasoning simpler, but it can also lead to misunderstandings.

The software in a computer, viz. a program, is both at the same time: a physical part of a physical artefact (for example in form of magnetism in the memory) and its own blueprint (in the form of a text in some higher or lower level programming language). The realisation of the latter consists of some form of translation, followed by loading the result into working memory. This is so well-understood and fast, that one often abstracts from it. Again, this can make reasoning simpler, but it can also lead to misunderstandings.

In our context, a computer program P, be it high or low level, should be considered as a blueprint as long as it is developed, written down, proved correct, or compiled. When "the same" program is loaded in program memory of a computer, however, it is a physical phenomenon that can be observed, usually as some form of magnetism. We write load(P) to state that program P had been loaded into the computer under discussion.

Programmable machines

Assume that a specification S is given, which specifies behaviour in terms of observables at some input/output ports of a controller. Assume we want to implement that controller by a suitably programmed computer. What does that mean in our framework? The artefact we want consists of two parts:

a computer 

That is a universal machine which "understands" a certain programming language. Maybe we already have that computer, maybe we will buy it.

a program 

This must turn the universal machine into a special-purpose machine such that the two together are an implementation of S. Of course, that program will have to be...

• written in the language the machine understands and
• loaded into that machine.

The correctness theorem for that artefact of two parts must be something like

UM(L) ∧ X ⇒ S

where UM(L) is the specification of a universal machine programmable in language L and X the specification of the program in its memory we need.

The denotational semantics sem(L) of a language L defines for each program P in L a predicate sem(L)(P), usually a huge conjunction.

A universal machine "executes" programs written in its language, provided these are loaded into its memory. So UM(L) is defined as follows:

UM(L) := ∀P. load(P)⇒sem(L)(P)

Obviously, our X must be:

∃P. load(P)∧(sem(L)(P)⇒S)

The complete correctness theorem

(∀P. load(P)⇒sem(L)(P)) ∧ (∃P. load(P)∧(sem(L)(P)⇒S)) ⇒ S

than reads: "A universal L-machine with loaded in its memory some program P, the semantics of which implies specification S, is an implementation of S."

If we want to consider the programming language L as a blueprint language we must define which specifications are satisfied by an arbitrary program P. But that is easy: the realisation of a blueprint P consists of P loaded into the computer:

P sat load(P)

If we can prove for some specific program P' that

sem(L)(P')⇒S

we can conclude that

P' sat load(P')∧(sem(L)(P')⇒S)

from which follows that P' satisfies our X.

Software engineers find it self-understanding that programs are loaded into a computer, which always is assumed to be available. When they say "P' satisfies S" they mean:

(sem(L)(P')⇒S) ∧ UM(L) ∧ load(P')