[Oberon] Deductive Installation - for Edsger W. Dijkstra

[Douglas G. Danforth]

(On 6 August 2002, Edsger W. Dijkstra, Professor Emeritus of Computer Sciences and Mathematics at the University of Texas at
Austin, died at his home in Nuenen, the Netherlands)

(The following could be a Ph.D. dissertation)

A computer operating system is installed by deduction or is deductively installed when the following hold.

An operating system has a required set of devices S.  Each device D is an abstraction which can have many specific instances of
which d is one (d in D, D in S).

A device d=(hardware, contoller, handler) is a triple not all elements of which need be present but for each device a specific
triple is specified.  If two devices differ in any of these components then they are different devices.

A device has an associated collection of 'probes' composed of sequences of 'pulses' over some set of hardware lines.  A probe
may not actually form these pulses but may be a command to a handler which causes the controller to form the pulses.  From here
on a, probe, is treated abstractly.

There is at least one special probe for each device called a 'reset' which puts the device into a known state.

A device 'transaction' consists of a probe followed by a 'response'.  A sequence of transactions is called a 'dialog'.

Every device has a (finite state) 'grammar' of dialogs.   

A dialog of d 'matches' a device if  all the probes and responses of the dialog are valid elements of the grammar of d.

At least one dialog of the grammar is called the 'test' dialog. An unknown device is 'accepted' by d if the test dialog of d
matches the device.  A device accepted by d is called d (with high probability).

It is also assumed that the test dialog puts an accepted device into an 'installed state'.  A device that is accepted is also
called 'installed'.

If at least one device d of D is installed then the abstract device D is installed.

If all devices D of S are installed then S is installed.

It is desired to find the weakest preconditions for the installation of each device that guarentees the correct installation of
system S.

-o-