[SystemSafety] Systematic and random error in systems

[Olwen Morgan]

Here's an illustration of the kind of elephant-in-the-room issue that 
hinders standardisation in software dependability: Consider the 
following C program:

#include <stdio.h>
#include <limits.h>

int main(void)
{
     return printf("\n%i\n", INT_MAX);
}

Now ask the question, "Is it portable?" Obviously the answer depends on 
what its purpose is and among which implementations of C you want it to 
be portable. Consider therefore the following definitions:

Let P denote this program. Let I and J denote respectively, those C 
implementations for which INT_MAX = 2^31-1 and let J denote the set of 
all C implementations. Obviously I is a subset of J. Now let O denote 
the proposition "output = 2^31-1". We can now define the Floyd-Hoare 
notation: TRUE { P } O, to mean that P always satisfies O on termination.

Now define: A program Q is portable among a set of implementations S and 
with respect to a correctness predicate C if and only if TRUE { Q } C 
for all implementations in S. (OK this needs to be generalised for 
programs that take specified input but it's the idea we're demonstrating 
here.)

Now we ask, is P portable among members of J with respect to O? Clearly 
it is not. But P is portable among members of I with respect to O. And 
of course, if O were replaced by O' the predicate "output = INT_MAX", 
the P would be portable among members of J with respect to O'.

This shows how, using the underlying theory of programming, we can 
easily define what it means for a program to be portable - and we note 
that portability is relative both to a specified set of implementations 
and with respect to a specified predicate.The elephant-in-the-room issue 
is that, so far, standardisation working groups have never adopted this 
kind of definition for dependability attributes. The underlying theory 
gives us a precise way to say what we mean by portability that most 
software engineers simply refuse to use.

Is it any wonder that standardisation is broken?


Olwen