Procedures, parameters, and abstraction: Separate concerns (Q1113659)

The paper argues that the notions of procedure, parametrization, and abstraction can be separated and that the result could be of practical use. The separation relies essentially on the embedding of procedural abstractions (specifications) within programs. The copy rule of ALGOL 60 gives significance to the procedure calls which are not yet executable code but only the specification, the specification itself being the text to copy. Using the standard axiomatic framework of Hoare and Dijkstra, the author proves that ``substitution'' by value, by result and by value/result are monotonic with respect to the (order) relation of refinement defined over the programs. The ``substitution'' by name cannot be treated, but one difficulty is located: aliasing is shown to be a non- monotonic construction. The aim of the paper is to give an orthogonal set of rules for the axiomatic treatment of procedures, parametrization, and abstraction. The independence of rules seems to both open up new possibilities and introduce new limitations for the considered notions.