Program Specification

A program is correct, Dijkstra insisted [1], only if it provably satisfies a given formal specification. The specification has been chosen for its pleasantness (to use Dijkstra's word): that is, a program satisfying the specification will satisfy the informal needs of the programmer's customers. The specification is located at the interface between need and satisfaction—the program's input-output interface. It acts as a firewall, rigorously isolating the programmer's correctness concern from the customers' need for an informal pleasantness that could corrupt the formality of the programming task. For a program to compute the GCD (Greatest Common Divisor) of two positive integers, the interface is two argument integers A and B, and a result integer C: the specification is "C is the GCD of A and B." On the other side of the interface, the customer judges GCD more pleasant than LCM (Lowest Common Multiple): but that is another world. The programmer need not—indeed, must not—be concerned with the customers' reasons: everything needed for correctness is in the specification.

For cyber-physical systems, too, software engineers may aspire to write provably correct programs. Here, a pleasant specification is one whose satisfying program ensures the governed world behaviour desired by stakeholders. Where is this specification firewall located? Necessarily, at the shared phenomena where sensors and actuators connect the formal to the non-formal—the machine's input-output interface to the governed world. The level of abstraction is low. If only state phenomena are shared at the interface, then in one run of the system, nothing is visible at this interface except an evolving trace of these state values. The trace is constrained by the physical properties of the governed world and by execution of a correct program: acceptable traces are exactly those corresponding to desired governed world behaviour. The specification stipulates only that the program, monitoring the sensors and controlling the actuators, ensures that the evolving trace is always an acceptable trace. The customer gets the desired governed world behaviour. The programmer need know nothing of this behaviour above the level of the machine side of the sensors and actuators.

For almost any real system, this reductionist specification is absurd, offering the programmer only incomprehensible stipulations about sensor and actuator states. Common sense—for a lift system, for example—demands a specification expressed in such abstractions as "Go to next floor up", "Close the doors", "Illuminate request button", and so on. After all, the specifiers must have considered these and similar abstractions in their process of arriving at the reductionist specification. But these abstractions have no direct physical realisation: there is no actuator available to the trace specification that can respond to the command "Go to next floor up". Deeper in the governed world, the abstraction level can be raised only by major physical changes far outside the remit and scope of software engineering. Is our goal—of formal program specification located strictly at the machine-world interface—therefore unachievable? The answer must be yes.

How can this be? If 'GCD' is a permissible abstraction in specifying the arithmetical program, why is 'Go to next floor up' not allowed in the lift system? Is the difference perhaps a consequence of inadequate development method? No, it is not. The difference is in the problem worlds of the two examples. The GCD program is about arithmetic, which is a formal and abstract system. 'GCD' is a permissible abstraction because the axioms and theorems of arithmetic are certain, and are known to the specifier, the programmer, and even to the customer who finds 'GCD' more pleasant than 'LCM'. In unpacking 'GCD' we may wish to refer to 'divides', 'remainder', 'zero', 'modulo' and even 'prime': these are potentially related notions, but their definitions and relationships present no challenge to mathematical certainty and shared knowledge. In contrast, the governed world of a cyber-physical system is neither abstract nor formal. In Einstein's words [2]: "As far as the propositions of mathematics refer to reality, they are not certain; and as far as they are certain, they do not refer to reality.” Knowledge of the governed world's modelled properties is neither universal nor eternal, but specific to the time, the place, and the purposes of the particular system in hand—and always contingent. Its scope includes specific physical domains and the causal links they effectuate. There can be no presumption that any of this is known to the software programmer.

This challenge is fundamental for every cyber-physical system. It provides the ultimate justification of many of the basic structuring ideas presented in this blog, and of the principle that development must rest on an iterative cooperation between those whose primary concerns lie in the governed world and those for whom they lie in the machine.

[1] E W Dijkstra; On the Cruelty of Really Teaching Computing Science; CACM Volume 32 Number 12, page 1414, December 1989.

[2] Albert Einstein; Sidelights on Relativity: Ether and Relativity: II Geometry and Experience; Methuen, 1922.

Links to other posts:
 ↑  Physical Bipartite System: The nature of a bipartite system
 → The ABC of Modelling: Axiomatic, Behavioural, and Consequential aspects