Massaging the program

Dated: 

8 February 1981

Given a specific function, called lambo, how do you prove that it is equal to its own inverse? Dijkstra's answer: by massaging a program that computes lambo. That is, by gradually transforming an original program that computes lambo into a symmetric program that is rather useless to the programmer but useful to the mathematician!

The final program is mathematically interesting because it almost immediately provides the reader with the theorem that had to be proved in the first place, namely that lambo's inverse is lambo itself. Unsurpisingly, the final program reveals the symmetry that the theorem expresses about the function lambo.

Dijkstra's programs, expressed in his guarded-command language, are non-terminating programs. That is, they continue to compute function values ad infinitum. The variables used in his programs become arbitrarily large.  Contrast this, then, with the practical programs that he used to write in the 1950s in order to solve problems in numerical analysis, i.e. programs that were actually run on finite computing machines.

For the details and lambo's definition in particular, please consult EWD776.

Tags: 

1 Comment

Dijkstra doesn't like metaphors or analogies

Another analogy used by dijkstra even though he was hostile to them. What pray tell does "massaging" have to do with programming? He also used this to describe functional programming too, and I understand what he means, but it is still an analogy.